perm filename PROVE1.NEW[1,JRA]7 blob
sn#142379 filedate 1975-01-31 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00005 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002
C00037 00003
C00074 00004 (PROG (Z1 Z2 R M)
C00110 00005
C00111 ENDMK
C⊗;
(DEFPROP NEWPROOF
(NIL NEWPROOF
ALLPOS
ALLNEG
ANCESTOR
SEARCH1
CONST
HERE
VAR
MKWRD
NEG
NEGBIT
POS
POSBIT
SEARCH
NUM
NEGL
APPENDIT
ANDOR
ASSOC1
ATTEMPT
AUTO
BAKSUB
BOOKEEP
BUILTED
BUILTED1
BUILTCH
BUILTCH1
CHOICE
CHOICE1
CLAUSES
CLAUSES2
CLAUSES1
CNF
CNF1
CNF2
CNF3
CNVT
CNVT2
CNVT3
COPY
COPYDELETED
*CL
DEMOD
DEM
DEPTH
DEPTH1
DEP DEP1
DEL
DOWN
EDIT
ERPRINT
ERPRIN1
EXPUNGE
FINI
FIXNEG
FIXQFF
FIXQFF1
GENSKOLEM
GETNAME
GETTERMS
GETVARS
GOLIST
INCLAUSES
INITIAL
INITIALAX
INITIALAX1
MAKVAR
MAKOVAR
MAPIT
MAX
MAXDEPTH MAXDEPTH1 MAXLENGTH
MEMC
MIN1
MINIMIZE
MIN
MKSYM
MODEL
NCONC1
NEGATE
NEGSGN
ONEGSGN
*NOPOINT
OCCUR
ORDER
ORDEREQUAL
PARMOD
PARMOD1
POTZ
PRECNF
PROOF1
PROVE
PRPAR
PRFPRINT
PRFPR1
PROOF
PTRS
PUNIFY
QUERY
REAL-LNGTH
REDUCER
RESOLVE
RESOLVE1
RESUNITP
RESUNITN
SET1
SET2
SET3
SETUP
SEARCH2
S2
SETQUERY
SETQUERY1
SETQUERY2
SETSUP
SUBS3TA
SUBS3T**
SUB*
SUBSKOL
SUPPORT
SUBSUME1
SUBS2T
SUBS3T
SUBSUME
SUBST1
TCOPY
TERMS
TERMS1
TERMS2
TIMEIT
TRY
TRY1
TRYIT
TRAVERSE
UNIT
UNITS
UNITRES
UNITREDUCT
UNITPN
UNIFY
UNI
UNION
UNWIND
UPDATE
UPGETL
UPGETL1
UPDATESTATE
UPIT
UPIT1
UP1A
UP1B
VINE
<)
VALUE)
(DEFPROP ALLPOS
(LAMBDA (C) (LIST (QUOTE NULL) (LIST (QUOTE CADAR) (CADR C))))
MACRO)
(DEFPROP ALLNEG
(LAMBDA (C) (LIST (QUOTE EQ) (LIST (QUOTE CADAR) (CADR C)) (LIST (QUOTE CDR) (CADR C))))
MACRO)
(DEFPROP ANCESTOR
(LAMBDA (X) (LIST (QUOTE CDDDAR) (CADR X)))
MACRO)
(DEFPROP SEARCH1
(LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) NIL))
MACRO)
(DEFPROP CONST
(LAMBDA (X) (LIST (QUOTE NULL) (LIST (QUOTE CDR) (CADR X))))
MACRO)
(DEFPROP HERE
(LAMBDA (X) (LIST (QUOTE CAAR) (CADR X)))
MACRO)
(DEFPROP VAR
(LAMBDA (L) (LIST (QUOTE NUMBERP) (CADR L)))
MACRO)
(DEFPROP MKWRD
(LAMBDA (L) (LIST (QUOTE CDDAR) (CADR L)))
MACRO)
(DEFPROP NEG
(LAMBDA (X) (LIST (QUOTE EQ) (QUOTE ESCAPE) (LIST (QUOTE CAR) (CADR X))))
MACRO)
(DEFPROP NEGBIT
(LAMBDA (X) (LIST (QUOTE CDDAAR) (CADR X)))
MACRO)
(DEFPROP POS
(LAMBDA (X) (LIST (QUOTE NOT) (LIST (QUOTE NEG) (CADR X))))
MACRO)
(DEFPROP POSBIT
(LAMBDA (X) (LIST (QUOTE CADAAR) (CADR X)))
MACRO)
(DEFPROP SEARCH
(LAMBDA (X) (LIST (QUOTE SEARCH2) (CADR X) (CADDR X) (CADR X)))
MACRO)
(DEFPROP NUM
(LAMBDA (C) (LIST (QUOTE CAAAR) (CADR C)))
MACRO)
(DEFPROP NEGL
(LAMBDA (C) (LIST (QUOTE CADAR) (CADR C)))
MACRO)
(DEFPROP APPENDIT
(LAMBDA(X Y)
(PROG NIL (COND (USINGFL (SETQ USING (CONS N2 (APPEND (REVERSE Y) USING))))) (RETURN (APPEND X Y))))
EXPR)
(DEFPROP ANDOR
(LAMBDA(C UNL EXL PF)
(PROG (Z1 Z2)
(SETQ Z1 (CADR C))
(SETQ Z2 (CADDR C))
(COND
((OR (AND (EQ (CAR C) (QUOTE AND)) PF) (AND (EQ (CAR C) (QUOTE OR)) (NOT PF)))
(RETURN (LIST (QUOTE AND) Z1 Z2)))
((EQ (CAR Z1) (QUOTE AND))
(RETURN
(LIST (QUOTE AND)
(CNF1 (LIST (QUOTE OR) (CADR Z1) Z2) UNL EXL T)
(CNF1 (LIST (QUOTE OR) (CADDR Z1) (COPY Z2)) UNL EXL T))))
((EQ (CAR Z2) (QUOTE AND))
(RETURN
(LIST (QUOTE AND)
(CNF1 (LIST (QUOTE OR) (CADR Z2) (COPY Z1)) UNL EXL T)
(CNF1 (LIST (QUOTE OR) (CADDR Z2) Z1) UNL EXL T))))
(T (RETURN (LIST (QUOTE OR) Z1 Z2))))))
EXPR)
(DEFPROP ASSOC1
(LAMBDA (X L) (COND ((NULL L) NIL) ((EQ (CDR X) (CDAAR L)) (CAR L)) (T (ASSOC1 X (CDR L)))))
EXPR)
(DEFPROP ATTEMPT
(LAMBDA(Z S C)
(PROG (NEWNAME SUPPORT
EDITSTRAT
LCL
LVL
CNT
LSTCLS
LLST
Z1
MERGE
ORDER
DEBUG
DEPTH
LENGTH
ANCESTRY
STRATEGY
STRAT
PMODEL
NMODEL
PFLG
PDEPTH
DLIST
XYZ
XYZ1
COND
UNAXP
UNAXN
SAT
EE
EE1
CLAUSES
SUBCLAUSES
COUNT)
(SETQ TBL (SET1 (APPEND PREFN INFN)))
(SET3 Z)
(SETQ Z (MINIMIZE Z))
(SETQ NEWNAME (INITIAL Z))
(SETQ CLAUSES Z)
(UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
(SETQ COND C)
(SETQ LVL 1)
(SETQ COUNT 0)
(SETQ Z (UNITPN Z))
(SETQ UNAXP (CAR Z))
(SETQ UNAXN (CDR Z))
(COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
(SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
(T (SETQ SUBCLAUSES CLAUSES)))
(SETQ LCL (LAST CLAUSES))
(SETQ LSTCLS LCL)
(SETQ XYZ (SETQ EE CLAUSES))
(SETQ EE1 (LAST CLAUSES))
BB (SETQ LLST (CONS (CAR XYZ) LLST))
(SETQ XYZ (CDR XYZ))
(COND (XYZ (GO BB)))
(SETQ Z1 (ERRSET (TRYIT)))
(COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
(EVAL
(LIST (QUOTE OUTC)
(LIST (QUOTE OUTPUT)
(QUOTE PRF)
(QUOTE DSK:)
(CONS (READLIST
(CONS (QUOTE N)
(CONS (SETQ PRNO (ADD1 PRNO))
FILENAM)))
(QUOTE PRF)))
NIL)))
(QUERY)
(PROOF LHP RHP)
(OUTC Z T)
(RETURN Z1))
(T (RETURN Z1)))))
EXPR)
(DEFPROP AUTO
(LAMBDA(X1)
(PROG ( N DLIST Z2 D M SAVEED SAVESTR)
(SETQ N 1)
(SETQ M (SETQ D 0))
A (SETQ M (MAX M (LENGTH (CDAR X1))))
(SETQ D (MAX D (DEPTH (CDAR X1))))
(SETQ Z2 (CAR X1))
(COND
((AND (EQ (LENGTH (CDR Z2)) 1) (EQ (CAADR Z2) EQUAL) (NOT (EQ (CADADR Z2) (CAR (CDDADR Z2)))))
(SETQ DLIST(CONS N DLIST))))
(SETQ X1 (CDR X1))
(COND((NULL X1)(GO B)))
(COND ((CDR X1)(SETQ N(ADD1 N)) (GO A)))
(SETQ M (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2))
B (COND ((NOT (GREATERP M 0)) (SETQ M 1)))
(SETQ Z2(ASSOC THEOREMNAME NEWNAME))
(SETQ D(ADD1 D))
(COND(STRAT(COND((ZEROP ITER)(SETQ ITER 1)(COND((NOT(EQ M 1))(SETQ M(ADD1 M)))(T(SETQ D(ADD1 D)
))))(T(SETQ D(ADD1 D))(SETQ ITER 0)))))
(COND(Z2
(SETQ SAVESTR (LIST @AND @ANCESTRY (LIST @SUPPORT THEOREMNAME))))
(T (SETQ SAVESTR (QUOTE ANCESTRY))))
(SETQ SAVEED
(LIST @OR (LIST @MAXDEPTH @(CDR C) D)
(LIST @MAXLENGTH @C M)))
(COND((AND EQUAL DLIST)(SETQ SAVEED(LIST @AND (LIST @DEMOD DLIST 4) SAVEED))))
(SETQ DEBUG T)
(COND
(EQUAL (SETQ SAVESTR (CONS (QUOTE AND) (CONS SAVESTR (LIST (LIST (QUOTE EQUALITY) EQUAL 3)))))))
(RETURN
(CONS SAVESTR SAVEED))
))
EXPR)
(DEFPROP AUTO
(NIL . T)
VALUE)
(DEFPROP BAKSUB
(LAMBDA(Z R)
(PROG ( U1 U4)
ED4 (COND ((NOT Z) (RETURN NIL)) ((OR (NOT (HERE (CAR Z))) (ATOM (CDR (ANCESTOR (CAR Z))))) (GO ED6A)))
(SETQ U1 R)
ED3 (SETQ U4 (CAR Z))
ED1 (COND ((SUBSUME (CAR U1) U4)(DEL U4) (GO ED4)))
ED6 (SETQ U1 (CDR U1))
(COND (U1 (GO ED1)))
ED6A (SETQ Z (CDR Z))
(GO ED4)
))
EXPR)
(DEFPROP BOOKEEP
(LAMBDA(L M N)
(PROG (U)
B1 (SETQ U M)
B3 (RPLACD (CDAAR U) (CONS 0 N))
(SETQ U (CDR U))
(COND ((NULL U) (RETURN (NCONC L M))))
(GO B3)))
EXPR)
(DEFPROP BUILTED
(LAMBDA (X) (LIST (QUOTE LAMBDA) (QUOTE (C)) (BUILTED1 X)))
EXPR)
(DEFPROP BUILTED1
(LAMBDA(X)
(COND ((ATOM X) X)
((ATOM (CAR X))
(COND ((EQ (CAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDR X)) (SETQ DLIST (*CL (CADR X)CLAUSES)) NIL)
(T (CONS (CAR X) (BUILTED1 (CDR X))))))
((EQ (CAAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDAR X)) (SETQ DLIST (*CL (CADAR X)CLAUSES)) (BUILTED1 (CDR X)))
(T (CONS (BUILTED1 (CAR X)) (BUILTED1 (CDR X))))))
EXPR)
(DEFPROP BUILTCH
(LAMBDA(X)
(PROG (Z)
(SETQ PFLG T)(SETQ ANCESTRY NIL)
(SETQ Z (BUILTCH1 X))
(RETURN
(COND ((OR (ATOM Z) (EQUAL Z (QUOTE (AND))) (EQUAL X (QUOTE (OR)))) NIL)
(T (LIST (QUOTE LAMBDA) (QUOTE (C1 C2)) Z))))))
EXPR)
(DEFPROP BUILTCH1
(LAMBDA(X)
(COND ((ATOM X)
(COND ((EQ X (QUOTE ANCESTRY)) (SETQ ANCESTRY T) NIL)
((EQ X (QUOTE NONE)) NIL)
((MEMQ X (QUOTE (VINE ALLPOS ALLNEG UNIT)))
(LIST (QUOTE OR) (LIST X (QUOTE C1)) (LIST X (QUOTE C2))))
(T X)))
((EQ (CAR X) (QUOTE SUPPORT)) (SETSUP (CDR X)) (QUOTE(OR (SUPPORT C2)(SUPPORT C1))))
((EQ (CAR X) (QUOTE MODEL)) (SETQ PMODEL (CADR X))
(SETQ NMODEL (CADDR X))
(QUOTE (OR (NOT (MODEL C1)) (NOT (MODEL C2)))))
((EQ (CAR X) (QUOTE DEFMODEL))
(LIST (QUOTE OR)
(LIST (QUOTE NOT) (LIST (CDR X) (QUOTE C1)))
(LIST (QUOTE NOT) (LIST (CDR X) (QUOTE C2)))))
((EQ (CAR X) (QUOTE ANCESTRY)) (SETQ ANCESTRY T) (BUILTCH1 (CDR X)))
((ATOM (CAR X)) (CONS (BUILTCH1 (CAR X)) (BUILTCH1 (CDR X))))
((EQ (CAAR X) (QUOTE EQUALITY)) (SETQ PFLG NIL)
(SETQ EQUAL (CADAR X))
(SETQ PDEPTH (CADDAR X))
(BUILTCH1 (CDR X)))
(T (CONS (BUILTCH1 (CAR X)) (BUILTCH1 (CDR X))))))
EXPR)
(DEFPROP CHOICE
(LAMBDA(X)
(PROG (Z Z1 Z2)
(COND ((NOT (HERE X)) (RETURN NIL)) (ANCESTRY (SETQ Z (CHOICE1 X LLST))) (T (SETQ Z CLAUSES)))
A (SETQ Z1 (CAR Z))
(COND
((OR (NOT (HERE Z1))
(AND PFLG (ALLPOS X) (ALLPOS Z1))
(AND (ALLNEG Z1) (ALLNEG X))
(AND STRATEGY (NOT (STRATEGY X Z1))))
NIL)
(T (SETQ Z2 (NCONC Z2 (LIST Z1)))))
(SETQ Z (CDR Z))
(COND ((OR (EQ Z X) (NULL Z)) (RETURN Z2)))
(GO A)))
EXPR)
(DEFPROP CHOICE1
(LAMBDA (L LL) (COND ((ATOM (CDR (ANCESTOR L))) LL) (T (NCONC (CDR (TRAVERSE L)) LL))))
EXPR)
(DEFPROP CLAUSES
(LAMBDA (U) (PROG (DEBUG) (SETQ DEBUG T) (RETURN (CLAUSES1 U 1))))
EXPR)
(DEFPROP CLAUSES2
(LAMBDA (U) (CLAUSES1 U CNT))
EXPR)
(DEFPROP CLAUSES1
(LAMBDA(U N)
(PROG NIL
(COND ((NOT DEBUG) (RETURN NIL)))
(COND ((NULL (CAR U)) (RETURN NIL)))
CL1 (COND ((NULL U) (RETURN NIL)))
(UP1A (CAR U) N)
CL2 (SETQ U (CDR U))
(SETQ N (ADD1 N))
(GO CL1)))
EXPR)
(DEFPROP CNF
(LAMBDA(C1)
(PROG (C)
(SETQ C (PRECNF C1))
(RETURN (CNF2 (COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) NIL NIL NIL)) (T (CNF1 C NIL NIL T)))))))
EXPR)
(DEFPROP CNF1
(LAMBDA(C UNL EXL PF)
(COND ((EQ (CAR C) (QUOTE NOT)) (CNF1 (CADR C) UNL EXL (COND (PF NIL) (T T))))
((MEMQ (CAR C) (QUOTE (AND OR)))
(ANDOR (LIST (CAR C) (CNF1 (CADR C) UNL EXL PF) (CNF1 (CADDR C) UNL EXL PF)) UNL EXL PF))
((OR (AND (EQ (CAR C) (QUOTE FA)) PF) (AND (EQ (CAR C) (QUOTE TE)) (NOT PF)))
(CNF1 (CADDR C) (APPEND (CADR C) UNL) EXL PF))
((OR (EQ (CAR C) (QUOTE FA)) (EQ (CAR C) (QUOTE TE)))
(CNF1 (CADDR C) UNL (APPEND (GENSKOLEM (CADR C) UNL) EXL) PF))
(PF (SUBSKOL C EXL))
(T (CONS ESCAPE (SUBSKOL C EXL)))))
EXPR)
(DEFPROP CNF2
(LAMBDA(C)
(COND ((EQ (CAR C) (QUOTE AND)) (APPEND (CNF2 (CADR C)) (CNF2 (CADDR C))))
((EQ (CAR C) (QUOTE OR)) (LIST (CNF3 C)))
(T (LIST (LIST C)))))
EXPR)
(DEFPROP CNF3
(LAMBDA (C) (COND ((NOT (EQ (CAR C) (QUOTE OR))) (LIST C)) (T (APPEND (CNF3 (CADR C)) (CNF3 (CADDR C))))))
EXPR)
(DEFPROP CNVT
(LAMBDA(Z)
(PROG (ZP ZN VARL VARNO)
(SETQ VARNO 0)
(COND
((EQ (LENGTH Z) 1)
(RETURN (COND ((EQ (CAAR Z) ESCAPE) (LIST (QUOTE NOT) (CNVT2 (CDAR Z)))) (T (CNVT2 (CAR Z)))))))
A1 (COND ((EQ (CAAR Z) ESCAPE) (GO AN1)))
(SETQ ZP (CNVT2 (CAR Z)))
AP1 (SETQ Z (CDR Z))
(COND ((NULL Z) (GO AN2)) ((EQ (CAAR Z) ESCAPE) (GO AN1)))
(SETQ ZP (LIST (QUOTE OR) (CNVT2 (CAR Z)) ZP))
(GO AP1)
AN1 (SETQ ZN (CNVT2 (CDAR Z)))
AN1B (SETQ Z (CDR Z))
AN1A (COND ((NULL Z) (GO AN2)))
(SETQ ZN (LIST (QUOTE AND) (CNVT2 (CDAR Z)) ZN))
(GO AN1B)
AN2 (COND ((NULL ZP) (RETURN (LIST (QUOTE NOT) ZN)))
((NULL ZN) (RETURN ZP))
(T (RETURN (LIST (QUOTE IMP) ZN ZP))))))
EXPR)
(DEFPROP CNVT2
(LAMBDA(X)
(COND ((ATOM X) X)
((VAR (CAR X)) (CONS (CNVT3 (CAR X)) (CNVT2 (CDR X))))
((CONST (CAR X)) (CONS (CAR X) (CNVT2 (CDR X))))
(T (CONS (CNVT2 (CAR X)) (CNVT2 (CDR X))))))
EXPR)
(DEFPROP CNVT3
(LAMBDA(X)
(PROG (Z)
(SETQ Z (ASSOC X VARL))
(COND (Z (RETURN (CDR Z))))
(SETQ VARL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARL))
(RETURN VARNO)))
EXPR)
(DEFPROP COPY
(LAMBDA (X) (COND ((ATOM X) X) (T (CONS (COPY (CAR X)) (COPY (CDR X))))))
EXPR)
(DEFPROP COPYDELETED
(LAMBDA (X) (LIST (CONS (CONS NIL (CDAR X)) (CDR X))))
EXPR)
(DEFPROP *CL
(LAMBDA (C X) (UPGETL1 C X (CONS (CONS (QUOTE CLAUSES) X) NEWNAME)))
EXPR)
(DEFPROP DEMOD
(LAMBDA(X L)
(PROG (S1 S2)
(SETQ S1 (CDAR X))
A (COND ((NEG (CAR S1)) (DEM (TCOPY (CDR (SETQ S2 (CDAR S1)))) 1 DDEPTH L))
(T (DEM (TCOPY (CDR (SETQ S2 (CAR S1)))) 1 DDEPTH L)))
(COND ((EQ (CAR S2) EQUAL) (ORDEREQUAL (CDR S2))))
(SETQ S1 (CDR S1))
(COND (S1 (GO A)))
(RETURN X)
))
EXPR)
(DEFPROP DEM
(LAMBDA (T1 M N L) (COND ((OR (NULL T1) (EQ N M)) NIL) (T (PROG2 (DEM (PTRS T1) (ADD1 M) N L) (SUB* T1 L)))))
EXPR)
(DEFPROP DEPTH
(LAMBDA(Z)
(PROG (Z1 Z2)
(SETQ Z1 0)
D1 (COND ((NEG (CAR Z)) (SETQ Z2 (CDDAR Z))) (T (SETQ Z2 (CDAR Z))))
(SETQ Z1 (MAX Z1 (DEPTH1 Z2)))
(SETQ Z (CDR Z))
(COND (Z (GO D1)))
(RETURN Z1)))
EXPR)
(DEFPROP DEPTH
(NIL . 10)
VALUE)
(DEFPROP DEPTH1
(LAMBDA(Z)
(PROG (Z1)
(SETQ Z1 0)
D1 (COND ((OR (VAR (CAR Z)) (CONST (CAR Z))) (GO D2)))
(SETQ Z1 (MAX Z1 (ADD1 (DEPTH1 (CDAR Z)))))
D2 (SETQ Z (CDR Z))
(COND (Z (GO D1)))
(RETURN Z1)))
EXPR)
(DEFPROP DEL
(LAMBDA (C) (RPLACA (CAR C) NIL))
EXPR)
(DEFPROP DOWN
(LAMBDA(N L)
(PROG NIL
(COND ((NOT (AND (NUMBERP N) (GREATERP N 0))) (RETURN NIL)))
D1 (SETQ N (SUB1 N))
(COND ((ZEROP N) (RETURN L)))
(SETQ L (CDR L))
(COND (L (GO D1)))
(RETURN NIL)))
EXPR)
(DEFPROP EDIT
(LAMBDA(U Z)
(PROG (RES1 U1 U4)
ED4 (COND ((NULL Z) (RETURN RES1)))
(SETQ U4 (CAR Z))
(COND ((EDITSTRAT U4) (GO ED2)))
(SETQ U1 SUBCLAUSES)
ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
ED6 (SETQ U1 (CDR U1))
(COND (U1 (GO ED1)))
(SETQ U1 (CDR Z))
(COND ((NULL U1) (GO ED5)))
ED3 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
ED7 (SETQ U1 (CDR U1))
(COND (U1 (GO ED3)))
ED5 (SETQ RES1 (CONS U4 RES1))
ED2 (SETQ Z (CDR Z))
(GO ED4)))
EXPR)
(DEFPROP ERPRINT
(LAMBDA (X) (COND (DEBUG (PRINT X))))
EXPR)
(DEFPROP ERPRIN1
(LAMBDA (X) (COND (DEBUG (PRIN1 X))))
EXPR)
(DEFPROP EXPUNGE
(LAMBDA (L) (PROG NIL A (COND ((NULL L) (RETURN NIL))) (DEL (CAR L)) (SETQ L (CDR L)) (GO A)))
EXPR)
(DEFPROP FINI
(LAMBDA(U R Z1 Z2 E)
(PROG (Z)
(COND (UFLG (SETQ R (UNITREDUCT R UNAXP UNAXN))))
(COND ((NULL R) (RETURN 0)) ((NULL (CAR R)) (PROOF Z1 Z2) (ERR (QUOTE (QED)))))
(SETQ COUNT (PLUS COUNT (LENGTH R)))
(SETQ R (EDIT U R))
(CLAUSES2 R)
(COND ((NULL R) (RETURN 0)))
(BAKSUB CLAUSES R)
(BOOKEEP E R (CONS Z1 Z2))
(SETQ Z (UNITPN R))
(SETQ UNAXP (APPEND (CAR Z) UNAXP))
(SETQ UNAXN (APPEND (CDR Z) UNAXN))
(RETURN (LENGTH R))))
EXPR)
(DEFPROP FIXNEG
(LAMBDA (X) (COND ((EQ (CAR X) ESCAPE) (LIST (QUOTE NOT) (COPY (CDR X)))) (T (COPY X))))
EXPR)
(DEFPROP FIXQFF
(LAMBDA(C)
(PROG (Z)
(SETQ Z (FIXQFF1 C NIL NIL NIL))
(COND ((NULL (CAR Z)) (RETURN C)) (T (RETURN (LIST (QUOTE FA) (CAR Z) C))))))
EXPR)
(DEFPROP FIXQFF1
(LAMBDA(C NEW FA TE)
(PROG (Z)
(COND ((NULL C) (RETURN (CONS NEW (CONS FA TE))))
((EQ (CAR C) (QUOTE FA)) (RETURN (FIXQFF1 (CADDR C) NEW (APPEND (CADR C) FA) TE)))
((EQ (CAR C) (QUOTE TE)) (RETURN (FIXQFF1 (CADDR C) NEW FA (APPEND (CADR C) TE))))
((EQ (CAR C) (QUOTE NOT)) (RETURN (FIXQFF1 (CADR C) NEW FA TE)))
((MEMQ (CAR C) (QUOTE (AND OR IMP EQUIV))) (SETQ Z (FIXQFF1 (CADR C) NEW FA TE))
(RETURN
(FIXQFF1 (CADDR C) (CAR Z) (CADR Z) (CDDR Z)))))
(SETQ Z (GETVARS (COND ((NEG C) (CDDR C)) (T (CDR C)))))
A (COND ((NULL Z) (RETURN (CONS NEW (CONS FA TE))))
((OR (MEMBER (CAR Z) NEW) (MEMBER (CAR Z) FA) (MEMBER (CAR Z) TE)) (GO B)))
(SETQ NEW (CONS (CAR Z) NEW))
B (SETQ Z (CDR Z))
(GO A)))
EXPR)
(DEFPROP GENSKOLEM
(LAMBDA(VARL UNL)
(PROG (Z)
A (COND ((NULL VARL) (RETURN Z)))
(SETQ Z (CONS (CONS (CAR VARL) (CONS (MKSYM) UNL)) Z))
(SETQ VARL (CDR VARL))
(GO A)))
EXPR)
(DEFPROP GETNAME
(LAMBDA(X L)
(PROG (Z)
(SETQ Z (ASSOC X L))
(COND (Z (RETURN (CDR Z))))
(PRINT X)
(PRINC (QUOTE IS-AN-UNBOUND-NAME))
(RETURN NIL)))
EXPR)
(DEFPROP GETTERMS
(LAMBDA (E NAMELIST)
(PROG (Z )
(SCANSET)
(START)
(SETQ Z (ERRSET (<TM>) T))
(SCANRESET)
(COND ((OR (NULL Z) (NULL (CAR Z))) (RETURN NIL)))
(SETQ XYZ (TOP))
(COND ((NOT (EQ (READ) (QUOTE FOR))) (RETURN NIL)))
(SCANSET)
(START)
(SETQ Z (ERRSET (<TM>) T))
(SCANRESET)
(COND ((OR (NULL Z) (NULL (CAR Z))) (RETURN NIL)))
(SETQ XYZ1 (TOP))
(COND ((NOT (EQ (READ) (QUOTE IN))) (RETURN NIL)))
(RETURN (UPGETL E NAMELIST))))
EXPR)
(DEFPROP GETVARS
(LAMBDA(C)
(PROG (Z)
A (COND ((VAR (CAR C)) (SETQ Z (CONS (CAR C) Z)))
((CONST (CAR C)) NIL)
(T (SETQ Z (APPEND (GETVARS (CDAR C)) Z))))
(SETQ C (CDR C))
(COND (C (GO A)))
(RETURN Z)))
EXPR)
(DEFPROP GOLIST
(NIL (EO . UEO1)
(AD . USA1)(CO . UTE1)
(DS . UDS1)
(CH . UCH1)
(SY . USY1)
(CU . UCU1)
(FL . UFL1)
(DI . UDI1)
(ST . UST1)
(HA . UST1)
(DE . UDE1)
(IN . UIN1)
(EV . UEV1)
(QU . UQU1)
(TR . UTR1)
(UP . UUP1)
(ME . UME1)
(SI . USI1)
(SE . USE1)
(DO . UDO1)
(CL . UCL1)
(SU . USU1)
(AN . UAN1)
(TE . UTE1)
(RE . URE1)
(SA . USA1)
(PA . UPA1)
(ED . UED1)
(US . UUS1)
(PR . UPR1)
(FU . UFL2)
(FD . UFL3)
(GO . UGO1)
(EX . UEX1)
(AB . UAB1)
(HE . UHE1))
VALUE)
(DEFPROP INCLAUSES
(LAMBDA NIL
(PROG (Z Z1 AXNO)
(SETQ AXNO (QUOTE AXIOM))
A (SCANSET)
(START)
(SETQ ZIN (ERRSET (<INPUT>) T))
(SCANRESET)
(COND ((OR (NULL ZIN) (NULL (CAR ZIN))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
(SETQ ZIN (TOP))
(COND ((EQ ZIN (QUOTE EMPTY)) (RETURN Z))
((ATOM ZIN) (PRIN1 ZIN) (SETQ AXNO (SETQ FNNAM ZIN)) (GO A))
((MEMQ (CAR ZIN) DECOP) (GO B)))
(OUT >S< ZIN)
(SETQ Z
(APPEND Z
(SETUP
(CNF (COND ((EQ AXNO THEOREMNAME) (LIST (QUOTE NOT) (FIXQFF ZIN))) (T (FIXQFF ZIN)))))))
(GO A)
B (SETQ Z1 (CDR (ASSOC (CAR ZIN) DECTBL)))
(COND ((EQ Z1 (QUOTE IVAR)) (MAKOVAR (SETQ IVAR (APPEND IVAR (CDR ZIN)))))
((EQ Z1 (QUOTE EQUAL)) (SETQ PFLG NIL) (SETQ EQUAL (CADR ZIN)))
(T (SET Z1 (APPEND (CDR ZIN) (EVAL Z1)))))
(OUT >INPUT< ZIN)
(GO A)))
EXPR)
(DEFPROP INITIAL
(LAMBDA(L)
(PROG (ST Z Z1 Z2)
A (SETQ Z (CDR (ANCESTOR (CAR L))))
(COND ((NOT (ATOM Z)) (PRINT (QUOTE LOSE-IN-INITIAL)) (ERR NIL))
((SETQ Z1 (ASSOC Z ST)) (RPLACD (LAST Z1) (LIST (CAR L))))
(T (SETQ ST (CONS (CONS Z (LIST (CAR L))) ST))))
(SETQ Z2 (CONS (CAR L) Z2))
(SETQ L (CDR L))
(COND (L (GO A)))
(RETURN (REVERSE (CONS (CONS NIL NIL) (CONS (CONS (QUOTE %INITIAL) (REVERSE Z2)) ST))))))
EXPR)
(DEFPROP INITIALAX
(LAMBDA(L)
(PROG (Z Z1 Z2 Z3 AXNO)
(SETQ AXNO (CAR L))
(SETQ L (CDR L))
A (SETQ Z (CAR (SETUP (LIST (COPY (CDAR L))))))
(SETQ Z1 (ANCESTOR (CAR L)))
(COND ((ATOM (CAR Z1)) (SETQ Z1 (CDR Z1))))
(SETQ Z2 (ANCESTOR Z))
(RPLACA Z2 Z1)
(RPLACD Z2 AXNO)
(SETQ Z3 (CONS Z Z3))
B (SETQ L (CDR L))
(COND ((NULL L) (RETURN (REVERSE Z3))) ((ATOM (CAR L)) (SETQ AXNO (CAR L)) (GO B)))
(GO A)))
EXPR)
(DEFPROP INITIALAX1
(LAMBDA(L1)
(PROG (Z L2 L)
(SETQ L L1)
B1 (SETQ L2 L)
A1 (COND ((EQ (CAR L) (CADR L2)) (RPLACD L2 (CDDR L2)) (GO A1)))
(SETQ L2 (CDR L2))
(COND (L2 (GO A1)))
(SETQ L (CDR L))
(COND (L (GO B1)))
(SETQ L L1)
B (SETQ Z (CDDAAR L))
(COND ((NULL (CAAAR L)) (RPLACA (CAAR L) (LENGTH (CDAR L))))
((NUMBERP (CAAAR L)) NIL)
(T (RPLACA (CAAR L) (CAAAAR L))))
(COND ((ATOM (CDDR Z)) (GO A)))
(RPLACD Z (CONS (CDR Z) (QUOTE DEDUCT)))
A (SETQ L (CDR L))
(COND (L (GO B)))
(RETURN L1)))
EXPR)
(DEFPROP MAKVAR
(LAMBDA(X)
(CDR(ASSOC X VARTBL)))EXPR)
(DEFPROP MAKOVAR
(LAMBDA(X)
(PROG (X1 *NOPOINT Z Z1 M)
(SETQ *NOPOINT T)
(SETQ X1 X)
D(SETQ OUTVAR(NCONC OUTVAR(LIST(CONS VARNO(CAR X1)))))
(SETQ VARTBL(NCONC VARTBL(LIST(CONS (CAR X1)VARNO))))
(SETQ X1 (CDR X1))
(SETQ VARNO(ADD1 VARNO))
(COND (X1 (GO D)))
B (SETQ Z (EXPLODE (CAR X)))
(COND ((NUMBERP (CAR (LAST Z))) (GO A)))
(SETQ M 1)
C(SETQ Z1(READLIST(APPEND Z(LIST M))))
(SETQ IVAR(CONS Z1 IVAR))
(SETQ OUTVAR(NCONC OUTVAR(LIST(CONS VARNO Z1))) )
(SETQ VARTBL(NCONC VARTBL(LIST(CONS Z1 VARNO))))
(COND ((LESSP M 11) (SETQ VARNO(ADD1 VARNO)) (SETQ M (ADD1 M)) (GO C)))
A (SETQ X (CDR X))
(COND (X (SETQ VARNO (ADD1 VARNO)) (GO B)))
(RETURN OUTVAR)))
EXPR)
(DEFPROP MAPIT
(LAMBDA(X XYZ N)
(PROG (Z Z1 Z2)
(SETQ Z (GETNAME X N))
(COND ((NULL Z) (RETURN NIL)))
A (SETQ ZIN (CAR Z))
(SETQ Z2 (ERRSET (XYZ ZIN) T))
(COND ((NULL Z2) (PRINT (QUOTE SCREWED-FIND)) (RETURN NIL))
((NULL (CAR Z2)) NIL)
(T (SETQ Z1 (CONS (CAR Z) Z1))))
(SETQ Z (CDR Z))
(COND (Z (GO A)))
(RETURN (REVERSE Z1))))
EXPR)
(DEFPROP MAX
(LAMBDA (X Y) (COND ((GREATERP X Y) X) (T Y)))
EXPR)
(DEFPROP MEMC
(LAMBDA(C L)
(PROG NIL
(COND ((NULL L) (RETURN NIL)) ((POS C) (GO A)))
B (COND ((POS (CAR L)) (RETURN NIL)) ((EQUAL C (CAR L)) (RETURN T)))
(SETQ L (CDR L))
(COND (L (GO B)))
(RETURN NIL)
A (COND ((POS (CAR L)) (RETURN (MEMBER C L))))
(SETQ L (CDR L))
(COND (L (GO A)))
(RETURN NIL)))
EXPR)
(DEFPROP MIN1
(LAMBDA(L)
(PROG (Z Z1)
(SETQ Z (CAR L))
M1 (SETQ Z1 (CDR L))
(COND ((NULL Z1)
(COND ((NUMBERP (CAR Z)) (RETURN NIL)) (T (SETQ Z1 (COPY Z)) (RPLACA Z 0) (RETURN Z1))))
((NUMBERP (CAAR Z1)) (GO M2))
((OR (NUMBERP (CAR Z)) (ORDER Z (CAR Z1))) (SETQ Z (CAR Z1))))
M2 (SETQ L (CDR L))
(GO M1)))
EXPR)
(DEFPROP MINIMIZE
(LAMBDA(Z3)
(PROG (Z1 Z2 Z4)
(SETQ Z2 (LIST (CAR Z3)))
ED2 (SETQ Z3 (CDR Z3))
(COND ((NULL Z3) (RETURN (REVERSE Z2))))
(SETQ Z4 (CAR Z3))
(SETQ Z1 Z2)
ED1 (COND ((SUBSUME (CAR Z1) Z4) (GO ED2)))
(SETQ Z1 (CDR Z1))
(COND (Z1 (GO ED1)))
(SETQ Z1 (CDR Z3))
ED4 (COND ((NULL Z1) (GO ED5)) ((SUBSUME (CAR Z1) Z4) (GO ED2)))
(SETQ Z1 (CDR Z1))
(GO ED4)
ED5 (SETQ Z2 (CONS Z4 Z2))
(GO ED2)))
EXPR)
(DEFPROP MIN
(LAMBDA (X Y) (COND ((LESSP X Y) X) (T Y)))
EXPR)
(DEFPROP MKSYM
(LAMBDA NIL
(PROG NIL
(SETQ FNLIST (CONS (READLIST (APPEND (EXPLODE FNNAM) (EXPLODE (SETQ FNNO (ADD1 FNNO))))) FNLIST))
(SETQ PREFN (CONS (CAR FNLIST) PREFN))
(RETURN (CAR FNLIST))))
EXPR)
(DEFPROP MODEL
(LAMBDA(C)
(PROG (Z)
(SETQ Z (CDR C))
M1 (COND ((NEG (CAR Z)) (GO M3)) ((MEMBER (CAAR Z) PMODEL) (SETQ SAT C) (RETURN T)))
M2 (SETQ Z (CDR Z))
(COND (Z (GO M1)))
(RETURN NIL)
M3 (COND ((MEMBER (CADAR Z) NMODEL) (SETQ SAT C) (RETURN T)))
(GO M2)))
EXPR)
(DEFPROP NCONC1
(LAMBDA (A B) (COND ((NULL A) B) ((NULL B) A) (T (RPLACD A B))))
EXPR)
(DEFPROP NEGATE
(LAMBDA(Z)
(PROG (BDY)
(COND ((EQ (LENGTH Z) 1) (SETQ BDY (FIXNEG (CAR Z))) (GO D)))
(SETQ BDY (LIST (QUOTE OR) (FIXNEG (CADR Z)) (FIXNEG (CAR Z))))
(SETQ Z (CDDR Z))
C (COND ((NULL Z) (GO D)))
(SETQ BDY (LIST (QUOTE OR) (FIXNEG (CAR Z)) BDY))
(SETQ Z (CDR Z))
(GO C)
D (RETURN (SET3 (SETUP (CNF (LIST (QUOTE NOT) (FIXQFF BDY))))))))
EXPR)
(DEFPROP NEGSGN
(NIL . ¬)
VALUE)
(DEFPROP ONEGSGN
(NIL . ¬)
VALUE)
(DEFPROP *NOPOINT
(NIL . T)
VALUE)
(DEFPROP OCCUR
(LAMBDA(X Z)
(PROG (Z1)
OC1 (SETQ Z1 (CAR Z))
(COND ((VAR Z1) (COND ((EQ X Z1) (RETURN T)) (T (GO OC2))))
((CONST Z1) (GO OC2))
((OCCUR X (CDR Z1)) (RETURN T)))
OC2 (SETQ Z (CDR Z))
(COND (Z (GO OC1)))
(RETURN NIL)))
EXPR)
(DEFPROP ORDER
(LAMBDA(X Y)
(COND ((POS X) (COND ((POS Y) (ORDERP (CAR X) (CAR Y))) (T T)))
((NEG X) (COND ((NEG Y) (ORDERP (CADR X) (CADR Y))) (T NIL)))))
EXPR)
(DEFPROP ORDEREQUAL
(LAMBDA(S)
(PROG NIL
(COND ((VAR (CAR S))
(COND ((VAR (CADR S)) (COND ((GREATERP (CADR S) (CAR S)) (GO A)) (T (RETURN NIL)))) (T (GO A))))
((CONST (CAR S))
(COND ((VAR (CADR S)) (RETURN NIL))
((CONST (CADR S)) (COND ((ORDERP (CAAR S) (CAADR S)) (GO A)) (T (RETURN NIL))))
(T (GO A))))
((OR (VAR (CADR S)) (CONST (CADR S))) (RETURN NIL))
((MAXDEPTH1(CDAR S)(DEPTH1(CDADR S)))(RETURN NIL)))
A (PROG (S1) (SETQ S1 (CADR S)) (RPLACA (CDR S) (CAR S)) (RPLACA S S1))))
EXPR)
(DE ORDEREQUAL1(X)(PROG(S1 S2)
(SETQ S1(CDAR X))B(SETQ S2(COND((NEG(CAR S1))(CDAR S1))(T(CAR S1))))
(COND((EQ(CAR S2 )EQUAL)(ORDEREQUAL (CDR S2))))
(SETQ S1(CDR S1))(COND(S1(GO B)))(RETURN X)))
(DEFPROP PARMOD
(LAMBDA(C D)
(COND ((ALLNEG C) (PARMOD1 D C)) ((ALLNEG D) (PARMOD1 C D)) (T (NCONC (PARMOD1 C D) (PARMOD1 D C)))))
EXPR)
(DEFPROP PARMOD1
(LAMBDA(C D)
(PROG (PF YC YD Z Z1 Z2 X Y Y1 Y2 PAR TS)
(SETQ YC (CDR C))
PAR1 (SETQ YD (CDR D))
(SETQ X (CAR YC))
(COND ((NEG X) (RETURN PAR))
((ORDERP (CAR X) EQUAL) (GO PAR2))
((NOT (EQ (CAR X) EQUAL)) (RETURN PAR)))
PAR3 PAR3A
(COND ((NEG (CAR YD)) (SETQ Z2 (CDAR YD))) (T (SETQ Z2 (CAR YD))))
(SETQ Y1 (CDDR X))
(SETQ Y2 (CADR X))
PAR3B
(COND ((VAR (CAR Y1)) (GO PAR7A)))
(SETQ Z (TERMS (CAAR Y1) (CDR Z2) PDEPTH))
(COND ((NULL Z) (GO PAR7A)))
PAR5 (SETQ Z1 Z)
PAR4 (COND
((CONST (CAR Y1))
(COND ((OR (VAR (CAAR Z1)) (NOT (EQ (CAAR Y1) (CAAAR Z1)))) (GO PAR7))
(T (SETQ TS (COPY Y2)) (GO PAR9))))
((OR (VAR (CAAR Z1)) (NOT (EQ (CAAR Y1) (CAAAR Z1)))) (GO PAR7)))
(SETQ Y (UNIFY (CDAR Y1) (CDAAR Z1)))
(COND (Y (SETQ Y (CDR Y)) (GO PAR6)))
PAR7 (SETQ Z1 (CDR Z1))
(COND (Z1 (GO PAR4)))
PAR7A
(COND ((NULL PF) (SETQ PF T) (SETQ Y1 (LIST Y2)) (SETQ Y2 (CADDR X)) (GO PAR3B)))
PAR7B
(SETQ YD (CDR YD))
(COND (YD (GO PAR3A)))
PAR2 (SETQ YC (CDR YC))
(COND (YC (GO PAR1)))
(RETURN PAR)
PAR6 (SETQ TS (CADR (SUBS3T* Y (LIST NIL Y2))))
PAR9 (SETQ PARRES (SUBS3TA Y Z2 (CAR Z1) TS))
(COND ((NEG (CAR YD)) (SETQ PARRES (CONS ESCAPE PARRES))))
(SETQ Y (UNION Y C D X (CAR YD)))
(COND ((NULL Y) (GO PAR7)))
(SETQ PAR (CONS (SET2 (CAR (COND (DLIST (DEMOD Y DLIST))(EQUAL(ORDEREQUAL1 Y)) (T Y))) TBL) PAR))
(GO PAR7)))
EXPR)
(DEFPROP POTZ
(LAMBDA(X)
(PROG (Z Z1)
(SETQ Z (POTZ1 X))
(COND ((SETQ Z1 (PMEMQ Z POTZTBL)) (RETURN Z1)))
(SETQ POTZTBL (CONS Z POTZTBL))
(RETURN Z)))
EXPR)
(DEFPROP PRECNF
(LAMBDA(X)
(COND ((EQ (CAR X) (QUOTE NOT)) (LIST (QUOTE NOT) (PRECNF (CADR X))))
((MEMQ (CAR X) (QUOTE (AND OR))) (LIST (CAR X) (PRECNF (CADR X)) (PRECNF (CADDR X))))
((MEMQ (CAR X) (QUOTE (FA TE))) (LIST (CAR X) (CADR X) (PRECNF (CADDR X))))
((EQ (CAR X) (QUOTE IMP)) (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X))))
((EQ (CAR X) (QUOTE EQUIV))
(LIST (QUOTE AND)
(LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X)))
(LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (COPY (CADDR X)))) (PRECNF (COPY (CADR X))))))
(T X)))
EXPR)
(DEFPROP PROOF1
(LAMBDA(L)
(PROG (Q X Y Z P P1)
(PRINC (QUOTE / ))
(PRINC (QUOTE / ))
(PRFPRINT (CDR L))
(SETQ P (ANCESTOR L))
(COND ((ATOM (CDR P)) (GO P3)))
(SETQ P1 (CDR P))
(SETQ P (CAR P))
(PRINC (QUOTE / ))
(PRINC 1)
(PRINC (QUOTE / ))
(PRINC 2)
(SETQ X 1)
(SETQ Y 2)
(SETQ Q (LIST (CONS X P) (CONS Y P1)))
P1 (SETQ Z (ANCESTOR (CDAR Q)))
(COND ((ATOM (CDR Z)) (PRINT (CAAR Q)) (PRFPRINT (CDDAR Q)) (PRIN1 (CDR Z)) (GO P2)))
(SETQ X (ADD1 Y))
(SETQ Y (ADD1 X))
(PRINT (CAAR Q))
(PRFPRINT (CDDAR Q))
(PRINC X)
(PRINC (QUOTE / ))
(PRINC Y)
(SETQ Q (NCONC Q (LIST (CONS X (CAR Z)) (CONS Y (CDR Z)))))
P2 (SETQ Q (CDR Q))
(COND ((NULL Q) (RETURN NIL)))
(GO P1)
P3 (PRIN1 (CDR P))
(RETURN (TERPRI))))
EXPR)
(DEFPROP PROVE
(LAMBDA (L) (PROG (AUTO) (SETQ AUTO T) (EVAL (CONS (QUOTE TRY1) L))))
FEXPR)
(DEFPROP PRPAR
(LAMBDA(L)
(PROG NIL
(CLAUSES CLAUSES)
(TERPRI)
P1 (PROOF1 (CAR L))
(TERPRI)
(TERPRI)
(SETQ L (CDR L))
(COND (L (GO P1)))
(RETURN NIL)))
EXPR)
(DEFPROP PRFPRINT
(LAMBDA(X)
(PROG NIL
(SETQ &&Z (FUNFLAT (LIST (LIST (OUTTST (CNVT X) (FUNCTION >S<))))))
(SETQ LAST NIL)
(FPRINT &&Z 0)))
EXPR)
(DEFPROP PRFPR1
(LAMBDA(L)
(PROG (Z)
(COND ((NEG L) (PRINC ONEGSGN) (SETQ L (CDR L))))
(PRINC (CAR L))
(SETQ L (CDR L))
(PRINC (QUOTE /())
P1 (COND ((VAR (CAR L))
(COND ((MINUSP (CAR L)) (PRINC (QUOTE Z)) (PRINC (MINUS (CAR L))))
(T (PRINC (QUOTE X))
(COND ((SETQ Z (ASSOC (CAR L) VARL)) (PRINC (CDR Z)))
(T (SETQ VARL (CONS (CONS (CAR L) (SETQ ONO (ADD1 ONO))) VARL)) (PRINC ONO))))))
((CONST (CAR L)) (PRINC (CAAR L)))
(T (PRFPR1 (CAR L))))
P2 (SETQ L (CDR L))
(COND ((NULL L) (PRINC (QUOTE /))) (RETURN NIL)))
(PRINC (QUOTE /,))
(GO P1)))
EXPR)
(DEFPROP PROOF
(LAMBDA(L R)
(PROG (Q Q1 X Z)
(SETQ LHP L)
(SETQ RHP R)
(RPLACA (MKWRD L) 1)
(RPLACA (MKWRD R) 2)
(SETQ X 2)
(SETQ Q (LIST L R))
(SETQ Q1 Q)
P1 (SETQ Z (ANCESTOR (CAR Q)))
(COND ((ATOM (CDR Z)) (COND ((NOT (ATOM (CAR Z))) (SETQ Z (CAR Z))) (T (GO P2)))))
(RPLACA (MKWRD (CAR Z)) (SETQ X (ADD1 X)))
(RPLACA (MKWRD (CDR Z)) (SETQ X (ADD1 X)))
(NCONC Q (LIST (CAR Z) (CDR Z)))
P2 (SETQ Q (CDR Q))
(COND (Q (GO P1)))
(PRINT (QUOTE NIL))
(PRINC (CAR (MKWRD (CAR Q1))))
(PRINC (QUOTE / ))
(PRINC (CAR (MKWRD (CADR Q1))))
(SETQ X 1)
A (COND
((EQ (CAR (MKWRD (CAR Q1))) X) (PRINT X)
(PRFPRINT (CDAR Q1))
(COND
((ATOM (CAR (ANCESTOR (CAR Q1)))) (PRIN1 (CAR (ANCESTOR (CAR Q1)))))
((ATOM (CDR (ANCESTOR (CAR Q1))))
(PRINC (CAR (MKWRD (CAAR (ANCESTOR (CAR Q1))))))
(PRINC (QUOTE / ))
(PRINC (CAR (MKWRD (CDAR (ANCESTOR (CAR Q1)))))))
(T (PRINC (CAR (MKWRD (CAR (ANCESTOR (CAR Q1))))))
(PRINC (QUOTE / ))
(PRINC (CAR (MKWRD (CDR (ANCESTOR (CAR Q1))))))))))
(SETQ Q1 (CDR Q1))
(SETQ X (ADD1 X))
(COND (Q1 (GO A)))))
EXPR)
(DEFPROP PTRS
(LAMBDA(X)
(PROG (Z)
A (COND ((VAR (CAAR X)) NIL) ((CONST (CAAR X)) NIL) (T (SETQ Z (APPEND (TCOPY (CDAAR X)) Z))))
(SETQ X (CDR X))
(COND (X (GO A)))
(RETURN Z)))
EXPR)
(DEFPROP PUNIFY
(LAMBDA(X Y)
(PROG (LC Z1 Z2 Z3 Z4 Z6 Z7)
(SETQ LC (LIST NIL))
U3 (SETQ Z1 (CAR X))
(SETQ Z2 (CAR Y))
(COND ((VAR Z1) (SETQ Z3 (SEARCH Z1 (CDR LC)))) (T (SETQ Z3 Z1)))
(COND ((VAR Z2) (SETQ Z4 (SEARCH Z2 (CDR LC)))) (T (SETQ Z4 Z2)))
(COND ((VAR Z3)
(COND ((VAR Z4) (GO UN1))
((CONST Z4) (GO UN3))
(T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z3 (COPY Z4)))) (GO UN2))
((NOT (VAR Z2)) (SETQ Z4 (SUBS3T* (CDR LC) Z4))))
(COND ((OCCUR Z3 (CDR Z4)) (RETURN NIL)) (T (GO UN3))))))
((VAR Z4) (RETURN NIL))
((AND (CONST Z3) (CONST Z4)) (COND ((NOT (EQ (CAR Z3) (CAR Z4))) (RETURN NIL)) (T (GO UN2))))
((EQ (CAR Z3) (CAR Z4)) (SETQ Z6 (CDR (SUBS3T* (CDR LC) Z3)))
(SETQ Z7 (CDR (SUBS3T* (CDR LC) Z4)))
(SETQ X (APPEND Z6 (CDR X)))
(SETQ Y (APPEND Z7 (CDR Y)))
(GO U3))
(T (RETURN NIL)))
UN1 (SUBS2T Z3 Z4 LC)
UN2 (SETQ X (CDR X))
(COND (X (SETQ Y (CDR Y)) (GO U3)))
(RETURN LC)
UN3 (SUBS2T Z4 Z3 LC)
(GO UN2)))
EXPR)
(DEFPROP QUERY
(LAMBDA NIL
(PROG NIL
(PRINT (QUOTE CHOICE-STRATEGY-IS:))
(OUTIT(CAR STRAT))
(PRINT (QUOTE EDIT-STRATEGY-IS:))
(OUTIT(CDR STRAT))
(PRINT (QUOTE ELAPSED-TIME))
(PRINC (QUOTE =))
(PRINC (TIMEIT))
(RETURN (TERPRI))))
EXPR)
(DEFPROP REAL-LNGTH
(LAMBDA(L)
(PROG (N)
(SETQ N 0)
A (COND ((NULL (CDR L)) (RETURN N)) ((HERE (CAR L)) (SETQ N (ADD1 N))))
(SETQ L (CDR L))
(GO A)))
EXPR)
(DE REENTER()(TRYIT))
(DEFPROP REDUCER
(LAMBDA(C L)
(PROG (Z Z1 Z2 Z3 C1)
(SETQ Z (CDAR C))
(SETQ Z2 (CDAAR C))
(SETQ C1 C)
(SETQ Z3 (SETQ Z1 (CONS NIL (CAR Z2))))
A (COND ((EQ L (CDR C1)) (GO B)))
(SETQ C1 (CDR C1))
(SETQ Z1 (CDR Z1))
(GO A)
B (RPLACD C1 (CDDR C1))
(COND ((EQ (CAR Z) L) (RPLACA Z (CDR L))))
(COND ((EQ (CDR Z2) (CDR Z1)) (RPLACD Z2 (CDDR Z2))))
(RPLACD Z1 (CDDR Z1))
(RPLACA Z2 (CDR Z3))
(RPLACA (CAAR C) (SUB1 (CAAAR C)))
(RETURN C)))
EXPR)
(DEFPROP RESOLVE
(LAMBDA(C D)
(COND ((OR (ALLNEG D) (ALLPOS C)) (RESOLVE1 C D))
((OR (ALLPOS D) (ALLNEG C)) (RESOLVE1 D C))
(T (NCONC (RESOLVE1 C D) (RESOLVE1 D C)))))
EXPR)
(DEFPROP RESOLVE1
(LAMBDA(C D)
(PROG (CB DB DB1 YC YD YD1 Z X Y RES)
(COND ((AND COND (EVAL COND)) (ERR (CDR LCL))))
(SETQ YC (CDR C))
(SETQ CB (POSBIT C))
(SETQ YD1 (NEGL D))
(SETQ DB1 (NEGBIT D))
(SETQ DB DB1)
(SETQ YD YD1)
RES1 (SETQ X (CAR YC))
(COND ((NEG X) (RETURN RES)))
(SETQ Y (CAR YD))
(COND ((ORDERP (CAR X) (CADR Y)) (GO RES3)) ((NOT (EQ (CAR X) (CADR Y))) (GO RES4)))
(SETQ YD1 YD)
(SETQ DB1 DB)
(GO RES2A)
RES2 (SETQ Y (CAR YD))
(COND ((NOT (EQ (CAR X) (CADR Y))) (GO RES3A)))
RES2A
(COND ((NOT (UNIFAB (CAR CB) (CAR DB))) (GO RES2B)))
(SETQ Z (UNIFY (CDR X) (CDDR Y)))
(COND ((NULL Z) (GO RES2B)))
(SETQ PARRES NIL)
(SETQ Z (UNION (CDR Z) C D X Y))
(COND ((NULL Z) (GO RES2B)) ((NULL (CAR Z)) (RETURN Z)))
(SETQ RES (CONS (SET2 (CAR (COND (DLIST (DEMOD Z DLIST))(EQUAL(ORDEREQUAL1 Z)) (T Z))) TBL) RES))
RES2B
(SETQ YD (CDR YD))
(COND (YD (SETQ DB (CDR DB)) (GO RES2)))
RES3A
(SETQ DB DB1)
(SETQ YD YD1)
RES3 (SETQ YC (CDR YC))
(COND (YC (SETQ CB (CDR CB)) (GO RES1)))
(RETURN RES)
RES4 (SETQ YD (CDR YD))
(COND (YD (SETQ DB (CDR DB)) (GO RES1)))
(GO RES3A)))
EXPR)
(DEFPROP RESUNITP
(LAMBDA(P TM L)
(PROG (Z)
A (SETQ Z (CDADAR L))
(COND ((EQ (CAR Z) P) (GO C)))
B (SETQ L (CDR L))
(COND (L (GO A)))
(RETURN NIL)
C (COND ((UNIFY (CDR Z) TM) (RETURN (LIST NIL))))
(GO B)))
EXPR)
(DEFPROP RESUNITN
(LAMBDA(P TM L)
(PROG (Z)
A (SETQ Z (CADAR L))
(COND ((EQ (CAR Z) P) (GO C)))
B (SETQ L (CDR L))
(COND (L (GO A)))
(RETURN NIL)
C (COND ((UNIFY (CDR Z) TM) (RETURN (LIST NIL))))
(GO B)))
EXPR)
(DEFPROP SET1
(LAMBDA(L)
(PROG (TBL N)
(SETQ N 1)
(SETQ ZERO (CDAR (SETU (LIST (CONS 0 0)))))
A (SETQ TBL (CONS (CONS (CAR L) N) TBL))
(SETQ L (CDR L))
(COND (L (SETQ N (ADD1 N)) (GO A)))
(RETURN (SETU TBL))))
EXPR)
(DEFPROP SET2
(LAMBDA(C L)
(PROG (X Z T1 T2 T3* T2* T3 Z1)
(SETQ T2 (SETQ T2* (LIST NIL)))
(SETQ T3 (SETQ T3* (LIST NIL)))
(SETQ X (CDR C))
S1 (SETQ Z (CDAR X))
(SETQ T1 NIL)
(COND ((NEG (CAR X)) (GO S2)))
S1A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
(T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
(SETQ T1 (CONS (CDAR (LAST L)) T1))))
(SETQ Z (CDR Z))
(COND (Z (GO S1A)))
(SETQ X (CDR X))
(RPLACD T2* (LIST (POTZ T1)))
(SETQ T2* (CDR T2*))
(COND (X (GO S1)))
S4 (COND ((EQ T2 T2*) (RPLACA T3 (CDR T3))) (T (RPLACA T3 (CDR T2)) (RPLACD T2* (CDR T3))))
(RPLACA (CAR C) (CONS (CAAR C) T3))
(RETURN C)
S2 (SETQ Z (CDDAR X))
(SETQ T1 NIL)
S2A (COND ((VAR (CAR Z)) (SETQ T1 (CONS ZERO T1)))
((SETQ Z1 (ASSOC (CAAR Z) L)) (SETQ T1 (CONS (CDR Z1) T1)))
(T (RPLACD (LAST L) (SETU (LIST (CONS (CAAR Z) (ADD1 (LENGTH L))))))
(SETQ T1 (CONS (CDAR (LAST L)) T1))))
(SETQ Z (CDR Z))
(COND (Z (GO S2A)))
(SETQ X (CDR X))
(RPLACD T3* (LIST (POTZ T1)))
(SETQ T3* (CDR T3*))
(COND (X (GO S2)))
(GO S4)))
EXPR)
(DEFPROP SET3
(LAMBDA(Z)
(PROG (E)
(COND ((OR (NULL Z) (MEMQ NIL Z)) (RETURN Z)))
(SETQ E Z)
S1 (COND ((HERE (CAR E)) (SET2 (CAR E) TBL)))
(SETQ E (CDR E))
(COND (E (GO S1)))
(RETURN Z)))
EXPR)
(DEFPROP SETUP
(LAMBDA(Z)
(PROG (BL Z1 Z2 Z3 Z4 Z5)
SET2 (SETQ Z3 (CAR Z))
(SETQ Z2 0)
(SETQ BL NIL)
(SETQ NO* NO)
(SETQ Z5 NIL)
S1 (SETQ Z4 (MIN1 Z3))
(COND ((NULL Z4) (GO S3)))
(UPIT Z4)
(COND ((MEMBER Z4 Z5) (GO S1)) ((POS Z4) (COND ((MEMBER (CONS ESCAPE Z4) Z5) (GO S4)))))
(SETQ Z2 (ADD1 Z2))
(SETQ Z5 (CONS Z4 Z5))
(GO S1)
S3 (SETQ Z3 NIL)
(SETQ Z4 Z5)
S2 (COND ((NEG (CAR Z4)) (SETQ Z3 Z4) (GO SET3)))
(SETQ Z4 (CDR Z4))
(COND (Z4 (GO S2)))
SET3 (SETQ Z5 (CONS (CONS Z2 (CONS Z3 (CONS 0 (CONS AXNO AXNO)))) Z5))
SET1 (SETQ Z1 (CONS Z5 Z1))
S4 (SETQ Z (CDR Z))
(COND (Z (GO SET2)))
(RETURN Z1)))
EXPR)
(DEFPROP SEARCH2
(LAMBDA (X L L1) (PROG NIL (SETQ KR1 (ASSOC X L)) (COND (KR1 (RETURN (CDR KR1)))) (RETURN L1)))
EXPR)
(DEFPROP S2
(LAMBDA(X Y Z)
(PROG (Z1)
(SETQ Z1 (CDR Z))
A (COND ((NULL Z1) (RETURN Z))
((VAR (CAR Z1)) (COND ((EQ (CAR Z1) Y) (RPLACA Z1 X))))
((CONST (CAR Z1)) NIL)
(T (RPLACA Z1 (S2 X Y (CAR Z1)))))
(SETQ Z1 (CDR Z1))
(GO A)))
EXPR)
(DEFPROP SETQUERY
(LAMBDA (X) (SETQUERY2 X NIL NIL))
EXPR)
(DEFPROP SETQUERY1
(LAMBDA(XYZ XYZ1)
(PROG (Z)
(SETQ Z (ERRSET (SETQUERY2 XYZ XYZ1 T)))
(COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (RETURN Z)))
(RETURN (CONS (QUOTE NOPROOF) (CAR Z)))))
EXPR)
(DEFPROP SETQUERY2
(LAMBDA(XX YY FLG)
(PROG (XYZ1 CHAN
Z
Z1
SAVESTR SAVEED)
(SETQ CHAN (OUTC NIL NIL))
(COND(FLG(SETQ SAVEED(CDR STRAT))(SETQ SAVESTR(CAR STRAT))))
(SETQ XYZ1 XX)
(COND ((NULL FLG) (GO SRA1)) ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
(PRINT SETQMESS)
(SETQ XX (UPDATE XX))
(SETQ XYZ1 XX)
SRA1 (COND ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
(PRINT (QUOTE HERE-ARE-THE-CLAUSES:))
AA (CLAUSES XX)
SRA (COND ((AND AUTO (NULL FLG)) (SETQ Z (AUTO XYZ1)) (OUTC CHAN NIL) (RETURN Z))
(AUTO (PRINT (QUOTE (STILL-AUTO (Y / N))))
(COND
((EQ (READ) (QUOTE Y)) (SETQ Z (CONS XYZ1 (AUTO XYZ1))) (OUTC CHAN NIL) (RETURN Z)))))
SR2A (PRINT (QUOTE THE-FOLLOWING-BUILTIN-STRATEGIES-ARE-AVAILABLE:))
(PRINT
(QUOTE "ANCESTRY VINE UNIT MODEL[POS ; NEG] DEFMODEL[NAME] P1
SUPPORT[#,..] EQUALITY[ID,#] "))
(PRINT (QUOTE CHOICE-STRATEGY-IS:))
(COND
(FLG (OUTIT SAVESTR)
(PRINT (QUOTE DO-YOU-WANT-TO-CHANGE-IT))
(SETQ Z (READ))
(COND ((EQ Z (QUOTE N)) (GO SRB)))))
(SCANSET)
(START)
(SETQ Z (ERRSET (<ST>) T))
(SCANRESET)
(COND ((OR (NULL Z) (NULL (CAR Z))) (PRINT (QUOTE SCREWED-STRATEGY)) (GO SR2A)))
(SETQ SAVESTR(SETQ ZIN (TOP)))
(OUTIT ZIN)
SRB (SETQ DEBUG T)
SRAA (PRINT (QUOTE EDIT-STRATEGY-IS:))
(COND
(FLG (OUTIT SAVEED)
(PRINT (QUOTE DO-YOU-WANT-TO-CHANGE-IT))
(SETQ Z (READ))
(COND ((EQ Z (QUOTE N)) (GO SRCA)))))
(SCANSET)
(START)
(SETQ Z1 (ERRSET (<ST>) T))
(SCANRESET)
(COND ((OR (NULL Z1) (NULL (CAR Z1))) (PRINT (QUOTE SCREWED-EDIT-STRATEGY)) (GO SRAA)))
(SETQ SAVEED (SETQ ZIN (TOP)))
(OUTIT ZIN)
SRCA (SETQ UFLG T)
(SETQ Z1
(CONS SAVESTR SAVEED))
(OUTC CHAN NIL)
(COND (FLG (RETURN (CONS XYZ1 Z1))) (T (RETURN Z1)))))
EXPR)
(DEFPROP SETSUP
(LAMBDA(X)
(PROG (Z)
(SETQ X (*CL X CLAUSES))
A (COND ((NULL X) (SETQ SUPPORT Z) (RETURN NIL)))
(SETQ Z (CONS (CDAR X) Z))
(SETQ X (CDR X))
(GO A)))
EXPR)
(DEFPROP SUBS3TA
(LAMBDA(L Z XX TS)
(PROG (X1 X2 X3 Z4)
(SETQ X1 (LIST (CAR Z)))
(SETQ X2 X1)
(GO SUB2)
SUB1 (RPLACD X2 (LIST X3))
(SETQ X2 (CDR X2))
SUB2 (SETQ Z (CDR Z))
(SETQ Z4 (CAR Z))
(COND ((NULL Z) (RETURN X1))
((EQ Z XX) (SETQ X3 TS) (GO SUB1))
((VAR Z4) (SETQ X3 (SEARCH Z4 L)) (GO SUB1))
((CONST Z4) (SETQ X3 Z4) (GO SUB1))
(T (SETQ X3 (SUBS3TA L Z4 XX TS)) (GO SUB1)))))
EXPR)
(DEFPROP SUBS3T**
(LAMBDA (L X) (COND ((NULL L) (SUBS3T (QUOTE ((-11 . -1))) X)) (T (SUBS3T L X))))
EXPR)
(DEFPROP SUB*
(LAMBDA(X L)
(PROG (S2 Z L1)
B (SETQ L1 L)
A (SETQ S2 (CDADAR L1))
(SETQ Z (UNI (LIST (CAR S2)) (LIST (CAAR X)) NIL))
(COND (Z (RPLACA (CAR X) (CADR (SUBS3T* Z (CONS NIL (CDR S2)))))))
(SETQ L1 (CDR L1))
(COND (L1 (GO A)))
(SETQ X (CDR X))
(COND (X (GO B)))))
EXPR)
(DEFPROP SUBSKOL
(LAMBDA (C EXL) (SUBS3T EXL C))
EXPR)
(DEFPROP SUPPORT
(LAMBDA (X) (PROG NIL (COND ((NOT (EQ LVL 1)) (RETURN T)) (T (RETURN (MEMBER (CDR X) SUPPORT))))))
EXPR)
(DEFPROP SUBSUME1
(LAMBDA(C CB D DB L)
(PROG (Z)
SUB5 (COND ((NEG (CAR C)) (GO SUB3))
((NEG (CAR D)) (RETURN NIL))
((EQ (CAAR C) (CAAR D)) (GO SUB1))
((ORDERP (CAAR C) (CAAR D)) (RETURN NIL))
(T (GO SUB2)))
SUB1 (COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDAR C) (CDAR D) L))) (T (GO SUB2)))
SUB4 (COND ((NULL Z) (GO SUB2)) ((NULL (CDR C)) (RETURN T)) ((SUBSUME1 (CDR C) (CDR CB) D DB Z) (RETURN T)))
SUB2 (SETQ D (CDR D))
(COND (D (SETQ DB (CDR DB)) (GO SUB5)))
(RETURN NIL)
SUB3 (COND
((NEG (CAR D))
(COND ((EQ (CADAR C) (CADAR D))
(COND ((UNIAB (CAR CB) (CAR DB)) (SETQ Z (UNI (CDDAR C) (CDDAR D) L)) (GO SUB4))
(T (GO SUB2))))
((ORDERP (CADAR C) (CADAR D)) (RETURN NIL))
(T (GO SUB2)))))
(SETQ D (CDR D))
(COND (D (SETQ DB (CDR DB)) (GO SUB3)))
(RETURN NIL)))
EXPR)
(DEFPROP SUBS2T
(LAMBDA(X Y Z)
(PROG (U Z1)
(COND ((EQ X Y) (RETURN Z)))
(SETQ U (CDR Z))
(GO S2)
S1 (SETQ Z1 (CDAR U))
(COND ((VAR Z1) (COND ((EQ Y Z1) (RPLACD (CAR U) X))))
((CONST Z1) NIL)
(T (RPLACD (CAR U) (S2 X Y Z1))))
(SETQ U (CDR U))
S2 (COND (U (GO S1)))
(RPLACD Z (CONS (CONS Y (COND ((OR (VAR X) (CONST X)) X) (T (COPY X)))) (CDR Z)))
(RETURN Z)))
EXPR)
(DEFPROP SUBS3T
(LAMBDA (L X) (COND ((NEG X) (CONS ESCAPE (SUBS3T* L (CDR X)))) (T (SUBS3T* L X))))
EXPR)
(DEFPROP SUBSUME
(LAMBDA(C D)
(COND ((OR (AND (ALLPOS C) (ALLNEG D)) (AND (ALLNEG C) (ALLPOS D))) NIL)
((OR (NOT (HERE C)) (NOT (HERE D))) NIL)
((NOT (GREATERP (NUM C) (NUM D))) (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))
(T NIL)))
EXPR)
(DEFPROP SUBST1
(LAMBDA(X Y Z)
(COND ((ATOM Z) (COND ((EQ Y Z) X) (T Z)))
((EQUAL Y Z) X)
(T (CONS (SUBST1 X Y (CAR Z)) (SUBST1 X Y (CDR Z))))))
EXPR)
(DEFPROP TCOPY
(LAMBDA (X) (COND ((NULL X) NIL) ((VAR (CAR X)) (TCOPY (CDR X))) (T (CONS X (TCOPY (CDR X))))))
EXPR)
(DEFPROP TERMS
(LAMBDA (X Y Z) (CDR (TERMS2 X Y Z)))
EXPR)
(DEFPROP TERMS1
(LAMBDA(L N)
(COND ((OR (ZEROP N) (NULL L)) NIL)
((OR (VAR (CAR L)) (CONST (CAR L))) (CONS L (TERMS1 (CDR L) N)))
(T (NCONC (LIST L) (TERMS1 (CDAR L) (SUB1 N)) (TERMS1 (CDR L) (SUB1 N))))))
EXPR)
(DEFPROP TERMS2
(LAMBDA(Z L N)
(PROG (Z1 T1 T2)
(SETQ T2 (SETQ T1 (LIST NIL)))
A (COND ((NULL L) (RETURN T1))
((VAR (CAR L)) (GO B))
((CONST (CAR L)) (COND ((EQ Z (CAAR L)) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2)))) (GO B))
((EQ N 1) (GO B)))
(SETQ Z1 (TERMS2 Z (CDAR L) (SUB1 N)))
(COND ((EQ (CAAR L) Z) (RPLACD T2 (LIST L)) (SETQ T2 (CDR T2))))
(COND ((CDR Z1) (RPLACD T2 (CDR Z1)) (SETQ T2 (LAST T2))))
B (SETQ L (CDR L))
(GO A)))
EXPR)
(DEFPROP TIMEIT
(LAMBDA NIL (DIFFERENCE (DIFFERENCE (TIME) (GCTIME)) TIME1))
EXPR)
(DEFPROP TRY
(LAMBDA (L) (PROG (AUTO) (EVAL (CONS (QUOTE TRY1) L))))
FEXPR)
(DEFPROP TRY1
(LAMBDA(L)
(PROG (
ITER PREFN EQUAL INFN INFPREDLET IVAR PREPREDLET FNNO FNNAM
VARTBL OUTVAR VARNO
FILENAM PRNO POTZTBL NEWNAME TBL TIME1 Z Z2 AXNO)
(SETQ INFN @(%))(SETQ FNNO 0)(SETQ FNNAM @AXIOM)
(SETQ VARNO 1)
(SETQ ITER(SETQ PRNO 0))
T2 (COND ((NULL L) (SETQ FILENAM (QUOTE (P R F))) (GO P3)))
(SETQ Z (CAR (LAST L)))
(SETQ FILENAM (EXPLODE (COND ((ATOM Z) Z) (T (CAR Z)))))
(EVAL (CONS (QUOTE INPUT) L))
(INC T)
P3 B (SETQ Z2 (INCLAUSES))
(INC NIL)
(COND ((NULL Z2) (RETURN NIL)))
(SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
(SETQ Z2 (ATTEMPT Z2 NIL NIL))
A (COND ((OR (NULL Z2) (EQ (CAR Z2) (QUOTE QED))) (RETURN (QUOTE *)))
((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL)))
((EQ (CAR Z2) (QUOTE ABORT))
(SETQ Z2 (ATTEMPT (INITIALAX1 (APPEND (CADR Z2) (CDDR Z2))) NIL NIL))))
(GO A)))
FEXPR)
(DEFPROP TRYIT
(LAMBDA NIL
(PROG (Z1 Z2 R M)
(SETQ CNT (ADD1 (LENGTH CLAUSES)))
(SETQ EE (CDR EE))
TRY3 (SETQ Z1 (CAR EE))
(COND ((NOT (HERE Z1)) (GO TRY7)))
(SETQ M (CHOICE Z1))
(COND ((NULL M) (GO TRY7)))
TRY2 (SETQ Z2 (CAR M))
(COND ((NOT (HERE Z1)) (GO TRY7)) ((NOT (HERE Z2)) (GO TRY8)))
TRY1 TRY1A
(COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)))
(SETQ R (RESOLVE Z1 Z2))
(COND ((NULL R) (GO TRY6)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
(SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY8)))
(SETQ R (PARMOD Z1 Z2))
(COND ((NULL R) (GO TRY8)))
(SETQ CNT (PLUS CNT (FINI CLAUSES R Z1 Z2 EE1)))
TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
(SETQ M (CDR M))
(COND (M (GO TRY2)))
TRY7 (SETQ EE (CDR EE))
(COND ((NOT (EQ EE (CDR EE1))) (GO TRY3)))
(PRINT (QUOTE COUNT))
(PRINT COUNT)
(PRINT (QUOTE LEVEL))
(PRINT LVL)
(SETQ LVL (ADD1 LVL))
(PRINT (QUOTE ELAPSED-TIME))
(PRINT (TIMEIT))
(COND ((CDR EE1) (SETQ EE1 (LAST EE1)) (GO TRY3)))
(PRINT (QUOTE NO-PROOF-FOUND))
(COND (AUTO (ERR (QUOTE NOPROOF))))
(UPDATE CLAUSES)
(COND ((CDR EE1) (SETQ EE (CDR EE1)) (SETQ EE1 (LAST EE1)) (GO TRY3)))
(ERR (QUOTE NOPROOF))))
EXPR)
(DEFPROP TRAVERSE
(LAMBDA(L)
(PROG (Z Z1 Z2)
(SETQ Z (ANCESTOR L))
(SETQ Z1 (CAR Z))
(SETQ Z (CDR Z))
(COND ((NOT (ATOM (CDR (ANCESTOR Z)))) (SETQ Z2 (TRAVERSE Z))))
(COND ((NOT (ATOM (CDR (ANCESTOR Z1)))) (SETQ Z2 (NCONC (TRAVERSE Z1) Z2))))
(RETURN (COND ((HERE L) (CONS L Z2)) (T Z2)))))
EXPR)
(DEFPROP UNIT
(LAMBDA (X) (EQ (NUM X) 1))
EXPR)
(DEFPROP UNITS
(LAMBDA(U)
(PROG (Z Z1)
(COND ((NULL U) (RETURN NIL)))
(SETQ Z U)
UN1 (COND ((EQ (NUM (CAR Z)) 1) (SETQ Z1 (CONS (CAR Z) Z1))))
(SETQ Z (CDR Z))
(COND (Z (GO UN1)))
(RETURN Z1)))
EXPR)
(DEFPROP UNITRES
(LAMBDA(C UP UN)
(PROG (C1 Z1 U Z RES)
(SETQ C1 C)
(COND ((AND (ALLPOS C) (NULL UN)) (RETURN NIL)) ((AND (ALLNEG C) (NULL UP)) (RETURN NIL)))
(COND
((UNIT C)
(RETURN
(COND ((ALLPOS C) (RESUNITP (CAADR C) (CDADR C) UN)) (T (RESUNITN (CADADR C) (CDDADR C) UP))))))
(COND ((NULL UN) (SETQ C (NEGL C)) (GO N)))
(SETQ C (CDR C))
B (SETQ Z1 (CAR C))
(COND ((NEG Z1) (GO N)))
(SETQ U UN)
A (COND ((NOT (EQ (CAR Z1) (CADADR (CAR U)))) (GO A1)))
(SETQ Z (UNI (CDDADR (CAR U)) (CDR Z1) NIL))
(COND ((NULL Z) (GO A1)) ((UNIT C1) (RETURN (LIST NIL))))
(SETQ RES (CONS (REDUCER C1 C) RES))
(GO A2)
A1 (SETQ U (CDR U))
(COND (U (GO A)))
A2 (SETQ C (CDR C))
(COND (C (GO B)) (T (RETURN RES)))
N (SETQ Z1 (CDAR C))
(SETQ U UP)
C (COND ((NULL U) (RETURN RES)))
C2 (COND ((NOT (EQ (CAR Z1) (CAADAR U))) (GO C1)))
(SETQ Z (UNI (CDADAR U) (CDR Z1) NIL))
(COND ((NULL Z) (GO C1)) ((UNIT C1) (RETURN (LIST NIL))))
(SETQ RES (CONS (REDUCER C1 C) RES))
(GO C3)
C1 (SETQ U (CDR U))
(COND (U (GO C2)))
C3 (SETQ C (CDR C))
(COND (C (GO N)) (T (RETURN RES)))))
EXPR)
(DEFPROP UNITREDUCT
(LAMBDA(R UP UN)
(PROG (Z UP1 UN1 C1 C2 RC1 RC2)
(SETQ UN1 (SETQ UP1 NIL))
(SETQ C1 (SETQ C2 R))
A (SETQ RC1 (SETQ RC2 NIL))
(COND ((NULL C2) (GO C1)) ((AND (NULL UP1) (NULL UN1)) (GO C)))
B (SETQ Z (UNITRES (CAR C2) UP1 UN1))
(COND ((NULL Z) (SETQ RC2 (CONS (CAR C2) RC2)))
((NULL (CAR Z)) (RETURN (LIST NIL)))
(T (SETQ RC1 (APPEND Z RC1))))
(SETQ C2 (CDR C2))
(COND (C2 (GO B)))
C1 (SETQ UP (APPEND UP1 UP))
(SETQ UN (APPEND UN1 UN))
C (SETQ Z (UNITRES (CAR C1) UP UN))
(COND ((NULL Z) (SETQ RC2 (CONS (CAR C1) RC2)))
((NULL (CAR Z)) (RETURN (LIST NIL)))
(T (SETQ RC1 (APPEND Z RC1))))
(SETQ C1 (CDR C1))
(COND (C1 (GO C)))
(COND ((NULL RC1) (RETURN RC2)))
(SETQ C2 RC2)
(SETQ C1 RC1)
(SETQ Z (UNITPN C1))
(COND ((AND (NULL (CAR Z)) (NULL (CDR Z))) (RETURN (APPEND RC1 RC2))))
(SETQ UP1 (CAR Z))
(SETQ UN1 (CDR Z))
(GO A)))
EXPR)
(DEFPROP UNITPN
(LAMBDA(X)
(PROG (P N)
A (COND
((UNIT (CAR X)) (COND ((ALLPOS (CAR X)) (SETQ P (CONS (CAR X) P))) (T (SETQ N (CONS (CAR X) N))))))
(SETQ X (CDR X))
(COND (X (GO A)))
(RETURN (CONS P N))))
EXPR)
(DEFPROP UNIFY
(LAMBDA(X Y)
(PROG (LC Z1 Z2 Z3 Z4 Z6 Z7)
(SETQ LC (LIST NIL))
U3 (SETQ Z1 (CAR X))
(SETQ Z2 (CAR Y))
(COND ((VAR Z1) (SETQ Z3 (SEARCH Z1 (CDR LC)))) (T (SETQ Z3 Z1)))
(COND ((VAR Z2) (SETQ Z4 (SEARCH Z2 (CDR LC)))) (T (SETQ Z4 Z2)))
(COND ((VAR Z3)
(COND ((VAR Z4) (GO UN1))
((CONST Z4) (GO UN3))
(T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z3 (COPY Z4)))) (GO UN2))
((NOT (VAR Z2)) (SETQ Z4 (SUBS3T* (CDR LC) Z4))))
(COND ((OCCUR Z3 (CDR Z4)) (RETURN NIL)) (T (GO UN3))))))
((VAR Z4)
(COND ((CONST Z3) (GO UN1))
(T (COND ((NULL (CDR LC)) (RPLACD LC (LIST (CONS Z4 (COPY Z3)))) (GO UN2))
((NOT (VAR Z1)) (SETQ Z3 (SUBS3T* (CDR LC) Z3))))
(COND ((OCCUR Z4 (CDR Z3)) (RETURN NIL)) (T (GO UN1))))))
((AND (CONST Z3) (CONST Z4)) (COND ((NOT (EQ (CAR Z3) (CAR Z4))) (RETURN NIL)) (T (GO UN2))))
((EQ (CAR Z3) (CAR Z4)) (SETQ Z6 (CDR (SUBS3T* (CDR LC) Z3)))
(SETQ Z7 (CDR (SUBS3T* (CDR LC) Z4)))
(SETQ X (APPEND Z6 (CDR X)))
(SETQ Y (APPEND Z7 (CDR Y)))
(GO U3))
(T (RETURN NIL)))
UN1 (SUBS2T Z3 Z4 LC)
UN2 (SETQ X (CDR X))
(COND (X (SETQ Y (CDR Y)) (GO U3)))
(RETURN LC)
UN3 (SUBS2T Z4 Z3 LC)
(GO UN2)))
EXPR)
(DEFPROP UNI
(LAMBDA(C D L)
(PROG (Z1 Z2 Z3)
UN2 (SETQ Z2 (CAR D))
(SETQ Z1 (SETQ Z3 (CAR C)))
(COND
((VAR Z1) (SETQ Z3 (SEARCH1 Z1 L))
(COND ((NULL Z3) (SETQ L (CONS (CONS Z1 Z2) L)) (GO UN1))
((VAR Z3) (COND ((EQ Z3 Z2) (GO UN1)) (T (RETURN NIL)))))))
(COND ((VAR Z2) (RETURN NIL))
((CONST Z2) (COND ((EQ (CAR Z2) (CAR Z3)) (GO UN1)) (T (RETURN NIL))))
((VAR Z1) (COND ((EQUAL Z2 Z3) (GO UN1)) (T (RETURN NIL))))
((EQ (CAR Z2) (CAR Z3)) (SETQ C (APPEND (CDR Z3) (CDR C)))
(SETQ D (APPEND (CDR Z2) (CDR D)))
(GO UN2))
(T (RETURN NIL)))
UN1 (SETQ C (CDR C))
(COND (C (SETQ D (CDR D)) (GO UN2)))
(COND (L (RETURN L)) (T (RETURN (LIST (CONS 64 64)))))))
EXPR)
(DEFPROP UNION
(LAMBDA(Z C D YC YD)
(PROG (BL L Z1 Z2 Z3 Z4 Z5 Z6 C1 C2 NEG RES M1 Z7 Z8)
(SETQ NO* NO)
(COND
(ORDER (COND (ANCESTRY (SETQ SAT C) (SETQ L YC)) ((EQ C SAT) (SETQ L YC)) (T (SETQ L YD)))
(COND ((< L (CDR SAT)) (RETURN NIL)))))
(SETQ M1 0)
(SETQ Z7 (ANCESTOR C))
(SETQ Z8 (ANCESTOR D))
(SETQ C (CDR C))
(SETQ D (CDR D))
(SETQ Z1 Z)
(SETQ Z2 Z)
(SETQ Z3 (SUBS3T** Z1 YC))
(SETQ Z4 (SUBS3T** Z2 YD))
UN1 (SETQ Z5 (SUBS3T** Z1 (CAR C)))
(COND ((OR (EQUAL Z3 Z5) (MEMC Z5 C1)) (SETQ M1 (ADD1 M1)) (GO UN1A))
((AND (NEG Z5) (MEMC (CDR Z5) C1)) (RETURN NIL)))
(SETQ C1 (CONS Z5 C1))
UN1A (SETQ C (CDR C))
(COND (C (GO UN1)))
UN2 (SETQ Z6 (SUBS3T** Z2 (CAR D)))
(COND ((AND PARRES (EQUAL Z4 Z6)) (SETQ Z6 PARRES) (GO UN2B))
((OR (EQUAL Z4 Z6) (MEMC Z6 C2)) (SETQ M1 (ADD1 M1)) (GO UN2A))
((NEG Z6) (COND ((OR (MEMC (CDR Z6) C1) (MEMC (CDR Z6) C2)) (RETURN NIL))))
((POS Z6) (COND ((MEMBER (CONS ESCAPE Z6) C1) (RETURN NIL)))))
UN2B (SETQ C2 (CONS Z6 C2))
UN2A (SETQ D (CDR D))
(COND (D (GO UN2)))
(SETQ Z2 0)
(COND ((NULL C1) (COND ((NULL C2) (RETURN (LIST NIL))) (T (SETQ Z1 C2) (GO UN7))))
((NULL C2) (SETQ Z1 C1) (GO UN7)))
(COND ((AND MERGE (EQ M1 2) (CDR Z7) (CDR Z8)) (RETURN NIL)))
UN5 (SETQ NEG RES)
(COND ((NULL C1) (SETQ Z1 C2) (GO UN7))
((NULL C2) (SETQ Z1 C1) (GO UN7))
((AND (POS (CAR C1)) (POS (CAR C2))) (GO UN3))
((AND (POS (CAR C1)) (NEG (CAR C2))) (GO UN6))
((OR (AND (NEG (CAR C1)) (POS (CAR C2))) (NOT (ORDERP (CADAR C1) (CADAR C2))))
(SETQ Z1 (CAR C1))
(SETQ C1 (CDR C1))
(GO UN4)))
UN6 (SETQ Z1 (CAR C2))
(SETQ C2 (CDR C2))
UN4 (UPIT Z1)
(COND ((MEMBER Z1 RES) (GO UN5)) (T (SETQ Z2 (ADD1 Z2)) (SETQ RES (CONS Z1 RES)) (GO UN5)))
UN7 (COND ((NULL Z1) (RETURN (LIST (CONS (LIST Z2 NEG) RES)))) ((MEMBER (CAR Z1) RES) (GO UN8)))
(SETQ Z2 (ADD1 Z2))
(UPIT (CAR Z1))
(SETQ RES (CONS (CAR Z1) RES))
(COND ((NEG (CAR Z1)) (SETQ NEG RES)))
UN8 (SETQ Z1 (CDR Z1))
(GO UN7)
UN3 (COND ((NOT (ORDERP (CAAR C1) (CAAR C2))) (SETQ Z1 (CAR C1)) (SETQ C1 (CDR C1)) (GO UN4A)))
(SETQ Z1 (CAR C2))
(SETQ C2 (CDR C2))
UN4A (UPIT1 (CDR Z1))
(COND ((MEMBER Z1 RES) (GO UN5A)))
(SETQ Z2 (ADD1 Z2))
(SETQ RES (CONS Z1 RES))
UN5A (COND ((NULL C1) (SETQ Z1 C2) (GO UN7)) ((NULL C2) (SETQ Z1 C1) (GO UN7)))
(GO UN3)))
EXPR)
(DEFPROP UNWIND
(LAMBDA(X1 X2 Y Z N)
(PROG (Z1 Z2)
(SETQ Z2 (ASSOC1 X1 Z))
(COND (Z2 (SETQ Z1 (CDR Z2)) (GO A)))
(NCONC Y (COPYDELETED X1))
(NCONC Z (LIST (CONS (LAST Y) N)))
(SETQ Z1 N)
(SETQ N (ADD1 N))
A (SETQ Z2 (ASSOC1 X2 Z))
(COND (Z2 (RETURN (CONS (CONS Z1 (CDR Z2)) N))))
(NCONC Y (COPYDELETED X2))
(NCONC Z (LIST (CONS (LAST Y) N)))
(RETURN (CONS (CONS Z1 N) (ADD1 N)))))
EXPR)
(SPECIAL E)
(DEFPROP UPDATE
(LAMBDA(E)
(PROG (USINGFL USING
CHAN1
ELOC
CHAN
AUTO
DL1
RF
XYZ
XYZ1
CMD
LOCFLG
Z
Z1
Z2
INCT
Z3
Z1R
Z2R
N1
R
N
NAME
NAMELIST
ZZ)
(SETQ CHAN (OUTC NIL NIL))
(SETQ AXNO (QUOTE INSERT))
(SETQ FNNAM (QUOTE EDI))
(SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
(SETQ N1 (LAST NAMELIST))
(SETQ INCT (INC NIL))
U9 (SETQ ELOC E)
(SETQ N 1)
U3 (UP1A (CAR ELOC) N)
U3A (TERPRI)
U3AA (SETQ CMD (READ))
(COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
U3B (COND ((NOT (ATOM CMD)) (GO UER2)))
U3C (SETQ CMD (EXPLODE CMD))
(COND ((EQ (LENGTH CMD) 1) (GO UER1))
((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
(GO U3A)
UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
(GO U3A)
UDI1 (SETQ Z1 (UPGETL E NAMELIST))
(COND ((NULL Z1) (GO U3A)))
(CLAUSES Z1)
(GO U3A)
USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
(SETQ Z NAMELIST)
USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
(SETQ Z (CDR Z))
(COND (Z (GO USY2)))
(GO U3A)
UFL2 (SETQ Z (QUOTE U))
(GO UFL4)
UFL3 (SETQ Z (QUOTE D))
(GO UFL4)
UFL1 (SETQ Z (CAR (EXPLODE (READ))))
UFL4 (SETQ Z2 405104)
(COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
(COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (GO U3A)))
(UPDATESTATE (CDDR Z))
(GO U3A)
UDE1 (SETQ Z2 (UPGETL E NAMELIST))
(COND ((NULL Z2) (GO U3A)))
(EXPUNGE Z2)
(GO U3A)
UIN1 (SETQ NAME (READ))
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((NULL Z2) (GO U3A)))
UIN1A
(COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
(NCONC Z1 Z2)
(GO U3A)
USU1 (SETQ Z1 (ERRSET (GETTERMS E NAMELIST)))
(COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
((NULL (CAR Z1)) (GO U3A)))
(SETQ Z3 NIL)
(SETQ Z1 (CAR Z1))
USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
(SETQ Z1 (CDR Z1))
(COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (SETQ Z2(SET3 (SETUP Z3))) (GO UIN1A)))
UUP1 (SETQ Z2 (READ))
(COND ((AND (NUMBERP Z2) (EQ (READ) (QUOTE ;))) (GO U8)) (T (GO UER2)))
UDO1 (SETQ Z2 (READ))
(COND ((AND (NUMBERP Z2) (EQ (READ) (QUOTE ;))) (GO U7)) (T (GO UER2)))
UAN1 (SETQ Z2 (UPGETL E NAMELIST))
UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
(SETQ Z2 (CDR Z2))
(GO UAN2)
UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
(INC INCT)
(OUTC CHAN NIL)
(SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
(SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
(RETURN (MINIMIZE (APPEND Z1 Z)))
USA1 (SETQ Z2 (UPGETL E NAMELIST))
(COND (Z2 (NCONC E Z2)))
(GO U3A)
UPA1 (SETQ Z1 (UPGETL E NAMELIST))
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
(COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
(COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
(SETQ Z3 Z1)
(SETQ Z DDEPTH)
(SETQ DDEPTH 22)
USI2 (DEMOD (LIST (CAR Z3)) Z2)
(SETQ Z3 (CDR Z3))
(COND (Z3 (GO USI2)))
(PRINT (QUOTE CLAUSES-ARE:))
(CLAUSES Z1)
(SETQ DDEPTH Z)
(GO U3A)
UCU1 (QUERY)
(GO U3A)
UDS1 (SETQ Z1 (READ))
(COND ((NOT (ATOM Z1)) (GO UDS3)))
UDS2 (COND
((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
(GO UDS2)))
UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
(GO U3A)
UEO1 (OUTC CHAN1 T)
(GO U3A)
UUS1 (SETQ NAME (QUOTE %USING))
(SETQ USINGFL T)
(SETQ USING NIL)
UUS3 (SETQ LOCFLG T)
UUS2 (SETQ Z2 (UPGETL E NAMELIST))
(SETQ USINGFL NIL)
(COND ((NULL Z2) (GO U3A)))
USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
(COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
(T (RPLACA (CAR N1) NAME)
(RPLACD (CAR N1) Z2)
(RPLACD N1 (CONS (CONS NIL NIL) NIL))
(SETQ N1 (CDR N1))))
(GO U3A)
USE1 (SETQ NAME (READ))
(SETQ LOCFLG NIL)
(GO UUS2)
UCL1 (SETQ Z (READ))
UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
(GO UCL2))
(T (GO U3A)))
UGO1 (SETQ Z1 (READ))
(COND ((NOT (NUMBERP Z1)) (GO UER2)))
(COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
(T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
UTR1 (SETQ AUTO NIL)
(GO UEX2)
UEX1 (SETQ AUTO T)
UEX2 (SETQ NAME (QUOTE LEMMA))
(SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
(COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
(SETQ Z2
(ATTEMPT (INITIALAX (CONS THEOREMNAME (APPEND XYZ USING)))
NIL
NIL))
(GO AT1A)
UST1 (STOP)
(GO U3A)
UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
(ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
U8 (COND ((EQ Z2 0) (GO U9)))
U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
(SETQ Z2 (DIFFERENCE Z2 5))
(SETQ ZZ 5)
U84 (SETQ Z N)
(SETQ Z3 (DIFFERENCE N ZZ))
(COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
(SETQ N Z3)
(SETQ Z3 ELOC)
(SETQ ELOC (DOWN N E))
(SETQ ZZ NIL)
(SETQ Z1 ELOC)
U81 (COND ((EQ Z1 Z3) (GO U82)))
(SETQ ZZ (CONS (CAR Z1) ZZ))
(SETQ Z1 (CDR Z1))
(GO U81)
U82 (COND ((NULL ZZ) (GO U83)))
(UP1A (CAR ZZ) (SUB1 Z))
(SETQ ZZ (CDR ZZ))
(SETQ Z (SUB1 Z))
(GO U82)
U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
(SETQ Z2 (PLUS Z2 N))
U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
(SETQ ELOC (CDR ELOC))
(SETQ N (ADD1 N))
(UP1A (CAR ELOC) N)
(COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
UPR1 (TERPRI)
(SETQ XYZ NIL)
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
(COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
(SETQ AXNO THEOREMNAME)
(SETQ Z3 (COND ((NULL XYZ) (NEGATE (CDAR Z2))) (T (SET3 (SETUP (CNF (LIST (QUOTE NOT) XYZ)))))))
(SETQ AXNO (QUOTE INSERT))
(SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
(COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
(SETQ NAME (QUOTE LEMMA))
(SETQ LOCFLG T)
(GO USE2)
UME1 (SETQ Z1 (UPGETL E NAMELIST))
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
(BAKSUB Z1 Z2)
(GO U3A)
UHE1 (PRINT MESSAGE)
(GO U3A)
URE1 (SETQ Z1 (UPGETL E NAMELIST))
(SETQ Z2 (UPGETL E NAMELIST))
U%RE1
(SETQ RF T)
URE1A
(COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
(SETQ Z1R Z1)
(SETQ Z2R Z2)
(SETQ Z3 NIL)
(COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
(COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
(COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
(COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
(SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
UR3A (SETQ Z2R (CDR Z2R))
(COND (Z2R (GO UR3)))
(SETQ Z1R (CDR Z1R))
(COND (Z1R (SETQ Z2R Z2) (GO UR3)))
UR3B (COND ((NULL Z3)
(COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
(T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
(RF (SETQ NAME (QUOTE RES)))
(T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
(SETQ Z2 Z3)
(SETQ LOCFLG T)
(GO AT2A)
UEV1 (PRINT (QUOTE EVAL-AWAITS))
(SETQ Z2 (ERRSET (EVAL (READ)) T))
(COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
(GO UEV1)
AT1A (UPDATESTATE STRAT)
(COND
((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
(PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
(PRINC NAME)
(GO U3A))
((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
(SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
(SETQ AUTO NIL)
(GO AT1A))
((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
(SETQ Z2 (CADR Z2))
AT2A (SETQ N 1)
AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
(SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
(PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
(PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
(PRIN1 NAME)
(CLAUSES Z2)
(GO USE2)))
EXPR)
(UNSPECIAL E)
(DEFPROP UPGETL
(LAMBDA(E N)
(PROG (C)
(SCANSET)
(START)
(SETQ C (ERRSET (<CLAUSES>) T))
(SCANRESET)
(COND ((OR (NULL C) (NULL (CAR C))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
(SETQ C (TOP))
(COND ((EQ C (QUOTE EMPTY)) (RETURN NIL)))
(RETURN (UPGETL1 C E N))))
EXPR)
(DEFPROP UPGETL1
(LAMBDA(C E N)
(PROG (N1 Z Z1 Z2 Z3 ZZ N2)
AS1 (SETQ Z (CAR C))
(COND ((ATOM Z)
(COND ((NUMBERP Z) (SETQ N2 (QUOTE CLAUSES))
(COND ((SETQ Z1 (DOWN Z E)) (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1)))))
(T (RETURN NIL))))
((SETQ Z1 (GETNAME Z N)) (SETQ N2 Z) (SETQ ZZ (APPENDIT ZZ Z1)))
(T (RETURN NIL))))
((EQ (CAR Z) (QUOTE STAT)) (GO AS10))
((EQ (CAR Z) (QUOTE FIND)) (GO AS20))
((EQ (CAR Z) (QUOTE DSK)) (GO AS30))
((SETQ Z1 (GETNAME (CAR Z) N)) (SETQ N2 (CAR Z)) (GO AS2))
(T (RETURN NIL)))
AS6 (SETQ C (CDR C))
(COND (C (GO AS1)) (T (RETURN ZZ)))
AS2 (SETQ Z2 (CADR Z))
(SETQ N1 (CAR Z))
(SETQ Z (CDR Z))
(SETQ Z3 Z1)
AS2A (COND ((NOT (NUMBERP Z2)) (PRINT (QUOTE NON-NUMERIC-ARG-FOR:)) (PRINC N1) (RETURN NIL)))
AS3 (SETQ Z2 (SUB1 Z2))
(COND ((ZEROP Z2) (GO AS4)))
(SETQ Z1 (CDR Z1))
(COND (Z1 (GO AS3)) (T (PRINT (QUOTE EXCEEDED-SIZE-OF:)) (PRINC N1) (RETURN NIL)))
AS4 (COND
((NOT (HERE (CAR Z1))) (PRINT N1)
(PRINC (QUOTE / ))
(PRINC (CAR Z))
(PRINC (QUOTE / ))
(PRINC (QUOTE HAS-BEEN-DELETED))
(RETURN NIL)))
(SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1))))
(SETQ Z (CDR Z))
(COND (Z (SETQ Z1 Z3) (SETQ Z2 (CAR Z)) (GO AS2A)))
(GO AS6)
AS10 (SETQ N2 (QUOTE INSERT))
(SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF(COPY (SETQ XYZ (FIXQFF (CDR Z)))))))))
(GO AS6)
AS20 (SETQ N2 (QUOTE MATCHES))
(SETQ Z (MAPIT (CADR Z) (LIST (QUOTE FUNCTION) (LIST (QUOTE LAMBDA) (QUOTE (C)) (CADDR Z))) N))
(COND ((NULL Z) (GO AS6)) (T (GO AS31)))
AS30 (SETQ N2 (QUOTE INPUT))
(SETQ ZIN (CDR Z))
(COND
((NULL (ERRSET (EVAL (LIST (QUOTE INPUT) (QUOTE DSK:) ZIN)))) (PRINT (QUOTE CONTINUING)) (GO AS6)))
(INC T)
(SETQ Z (INCLAUSES))
(INC NIL)
(COND ((NULL Z) (RETURN NIL)))
AS31 (SETQ ZZ (APPENDIT ZZ Z))
(GO AS6)))
EXPR)
(DEFPROP UPDATESTATE
(LAMBDA(L)
(PROG NIL
(SETQ STRATEGY(BUILTCH(CAR L)))
(SETQ EDITSTRAT(BUILTED(CDR L)))
(SETQ STRAT L)
))
EXPR)
(DEFPROP UPIT
(LAMBDA (C) (COND ((NEG C) (UPIT1 (CDDR C))) (T (UPIT1 (CDR C)))))
EXPR)
(DEFPROP UPIT1
(LAMBDA(Z)
(PROG (Z1 Z2)
MAX2 (SETQ Z2 (CAR Z))
(COND ((VAR Z2) (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
((GREATERP Z2 NO*) NIL)
(T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO)))
(GO MAX1))
((CONST Z2) (GO MAX1))
(T (UPIT1 (CDR Z2))))
MAX1 (SETQ Z (CDR Z))
(COND (Z (GO MAX2)))
(RETURN NO)))
EXPR)
(DEFPROP UP1A
(LAMBDA(X N)
(PROG NIL
(TERPRI)
(PRINC N)
(PRINC (QUOTE / ))
(COND ((HERE X) (PRFPRINT (CDR X))) (T (PRINC (QUOTE *DE*))))
(RETURN NIL)))
EXPR)
(DEFPROP UP1B
(LAMBDA (X N) (PROG NIL (TERPRI) (PRINC N) (PRINC (QUOTE / )) (PRFPRINT (CDR X))))
EXPR)
(DEFPROP VINE
(LAMBDA (X) (ATOM (CDR (ANCESTOR X))))
EXPR)
(DEFPROP <
(LAMBDA(L X)
(PROG (Z Z1 Z2)
(SETQ Z X)
(COND ((NEG L) (SETQ L (CADR L)) (SETQ Z2 T)) (T (SETQ L (CAR L))))
A1 (SETQ Z1 (CAR Z))
(COND ((NEG Z1) (SETQ Z1 (CADR Z1))) (T (SETQ Z1 (CAR Z1))))
(COND ((NOT (ORDERP L Z1)) (GO A2))
((OR (AND (NOT Z2) (MEMBER Z1 PMODEL)) (AND Z2 (MEMBER Z1 NMODEL))) (RETURN T)))
A2 (SETQ Z (CDR Z))
(COND (Z (GO A1)))
(RETURN NIL)))
EXPR)
(DE MAXLENGTH(X N)(GREATERP (NUM X) N))
(DEFPROP MAXDEPTH
(LAMBDA(Z N)
(PROG NIL
D1 (COND ((MAXDEPTH1 (COND ((NEG (CAR Z)) (CDDAR Z)) (T (CDAR Z))) N) (RETURN T)))
(SETQ Z (CDR Z))
(COND (Z (GO D1))) (RETURN NIL)))
EXPR)
(DEFPROP MAXDEPTH1
(LAMBDA(Z N)
(PROG NIL
D1 (COND ((OR (VAR (CAR Z)) (CONST (CAR Z))) (GO D2))
((EQ N 1) (RETURN T))
((MAXDEPTH1 (CDAR Z) (SUB1 N)) (RETURN T)))
D2 (SETQ Z (CDR Z))
(COND (Z (GO D1)))
(RETURN NIL)))
EXPR)
(DEFPROP DEP
(LAMBDA(L)
(PROG (C1 C2)
(SETQ C1 (CDR C))
A (SETQ C2 (COND ((NEG (CAR C1)) (CDDAR C1)) (T (CDAR C1))))
(COND ((DEP1 C2 (COPY L)) (RETURN T)))
(SETQ C1 (CDR C1))
(COND (C1 (GO A)))
(RETURN NIL)))
FEXPR)
(DEFPROP DEP1
(LAMBDA(C L1)
(PROG (L Z)
A(SETQ L (COPY L1)) (COND ((VAR (CAR C)) (GO B)))
(SETQ Z (ASSOC (CAAR C) L))
(COND ((NULL Z) NIL) ((EQ (CDR Z) 1) (RETURN T)) (T (RPLACD Z (SUB1 (CDR Z)))))
(COND ((NULL (CDAR C)) NIL) ((DEP1 (CDAR C) L) (RETURN T)))
B (SETQ C (CDR C))
(COND (C (GO A)))
(RETURN NIL)))
EXPR)